что означает ошибка Изабель Не удается обновить законченную теорию "HOL.Finite_Set" означает?

Question

Я пытаюсь использовать теорию Finite_Set.thy, но когда я импортирую ее

imports "$ISABELLE_HOME/SRC/HOL/Finite_Set"

, теория, над которой я работаю, не анализируется. Когда я открываю саму теорию, я получаю следующую ошибку:

Невозможно обновить законченную теорию "HOL.Finite_Set"

Я не уверен, что это значит (или если это связано) или что я могу с этим поделать.

Answer 1

Аналогичный вопрос уже задавался в списке рассылки Isabelle

Finite_Set является частью HOL и не может быть отредактирован (и вы не можете щелкнуть по нему, чтобы открыть определения и т. Д. ). Вы должны импортировать Main (он же HOL.Main) вместо только Finite_Set.

Если вы действительно хотите импортировать только Finite_Set, вы должны импортировать через HOL.Finite_Set, а не указывать полный путь.

Однако это не должно быть причиной вашей проблемы.