Setting [no_vars] theory-wide

Question

I have an Isabelle theory that collects all my results and only presents them, so I’d currently apply [no_vars] to all my @thm antiquotations. (This suppresses the question marks in the schematic variables which are undesirable in the final presentation.)

Is there a way to make Isabelle use no_vars once for the whole theory?

Answer 1

I think the canonical way (whatever that means) is to add such options to your session ROOT. Either globally, e.g.,

session A = B +
  options [show_question_marks = false]
  theories
    ...

or per theory, e.g.,

session A = B +
  theories [show_question_marks = false]
    T1
  theories
    T2
    ...

Answer 2

The magic invocation is

declare [[show_question_marks = false]]

as documented in the section “Details of printed output” in isar-ref.pdf.