CODEWITHSUNDEEP
presentationisabelle
Joachim Breitner
Joachim Breitner

Reputation: 25763

Setting [no_vars] theory-wide

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?

Upvotes: 2

Views: 48

Answers (2)

chris
chris

Reputation: 5018

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
    ...

Upvotes: 2

Joachim Breitner
Joachim Breitner

Reputation: 25763

The magic invocation is

declare [[show_question_marks = false]]

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

Upvotes: 2

Related Questions