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?
You can set \isabellestyle{it} in root.tex