Исследуйте законченные теории в Изабель

Question

Я хочу увидеть определения в файле теории векторных пространств из Изабель / HOL. В этой теме списка рассылки Изабель объясняется, как это сделать с помощью команды: isabelle make HOL-Base.

Я работаю под Windows 10. Думаю, приведенная выше команда предназначена для Linux. Как я могу получить такой же эффект в моей системе?

Answer 1

Попробуйте запустить Изабель из командной строки с помощью isabelle jedit -l Pure (инструменты командной строки вызываются через Isabelle2018\Cygwin-Terminal.bat в Windows).Теперь Isabelle / Pure используется в качестве базового изображения вместо Isabelle / HOL.Затем загрузите файл теории, который вы хотите проверить, из установочного каталога Isabelle (HOL находится в <isabelle-dir>/src/HOL)