У меня есть теория Изабель, которая собирает все мои результаты и представляет только их, поэтому сейчас я бы применил [no_vars] ко всем своим @thm антикавычкам. (Это подавляет вопросительные знаки в схематических переменных, которые нежелательны в окончательной презентации.)
Есть ли способ заставить Изабель использовать no_vars один раз для всей теории?
Я думаю, что каноническим способом (что бы это ни значило) является добавление таких опций в вашу сессию ROOT. Либо глобально, например,
session A = B +
options [show_question_marks = false]
theories
...
или по теории, например,
session A = B +
theories [show_question_marks = false]
T1
theories
T2
...
declare [[show_question_marks = false]], как это делал Иоахим, локально или ко всем теориям, импортирующим теорию, декларирующую этот атрибут?
- person Hibou57; 29.04.2014
declare, включена в другую, то и в другой не будет вопросительных знаков. В этом смысле вариант, который я показал выше, является более гибким (вы можете просто активировать/деактивировать некоторые настройки для конкретной теории, не влияя на более поздние).
- person chris; 29.04.2014
T1 во втором списке теорий (где мне нужны настройки по умолчанию). А учитывая, что я настраиваю другой синтаксис вывода (например, переводы) в самом файле теории, я предпочитаю и его.
- person Joachim Breitner; 29.04.2014
Магический призыв это
declare [[show_question_marks = false]]
как описано в разделе «Подробности печатных материалов» в isar-ref.pdf.
