При вводе утверждений доказательства в файл теории Изабель (2020), например,
from ‹prime p › have p: "1 < p "
приложение интерфейса jEdit выдает всплывающую подсказку, предлагающую вставить команду открытия картуша \<open>, когда я набираю кавычки. Как вы можете видеть в строке выше, я разрешал это, и, похоже, это разрешено. Документация Изабель, кажется, рассматривает внутренний синтаксис как вложенную категорию, которая, кажется, допускает разграничение с помощью кавычек или с помощью вложения картуша \<open ... \<close>.
Есть ли в этом обратная сторона? Оператор imports требует цитирования ссылки на файл теории HOL-Computational_Algebra.Primes с форматом module.theory и не будет принимать картуш там, но теоретически утверждения, безусловно, кажутся эквивалентными.
