Søren Debois
Søren Debois

Reputation: 5688

How do I remove quotes/cartouches from document output on Isabelle?

Consider this snippet:

  lemma no_lift:
    assumes ‹∀L . ⟦γ L⟧ ≠ set L›     ― ‹Miner \<^term>‹γ› is non-trivial.›
    defines ‹γ' P N ≡ γ P›           
    shows ‹∀P. ∃N. set N ∩ ⟦γ' P N⟧ ≠ {}›   

When I generate latex or HTML output locally, the cartouches remain in the output. When I look at proof documents in the AFP, it seems the cartouches and quotes have been stripped.

How can I strip quotes and cartouches from document output?

Upvotes: 0

Views: 56

Answers (1)

Peter Zeller
Peter Zeller

Reputation: 2296

You can set \isabellestyle{it} in root.tex

Upvotes: 1

Related Questions