Email Gateway (Dec 31 2022 at 13:10): Email Gateway (Dec 31 2022 at 13:10):From: "C. Diekmann" <diekmann@net.in.tum.de>
Howdy Isabelle Experts,
I have a theory as follows:
lemma ‹2+3 = 5› by simp
lemma "2+3 = 5" by simp
The first lemma is delimited by cartouches, the second is delimited by
quotes.
When I build the proof document outline, I see the following:
lemma ‹2 +3 = 5›
lemma 2 +3 = 5
The first lemma gets printed with cartouches, the second lemma gets printed
without any delimiters.
This makes the document look inconsistent.
I try to keep my theories as consistent as possible by running
bin/isabelle update -D . -o update_control_cartouches -o
update_inner_syntax_cartouches regularly. But I still feel the document
looks slightly inconsistent. For example, the document antiquotation
\<term>‹2 +3 = 5› never prints the delimiting cartouches. Yet, the document
antiquotation @{lemma [source=true] ‹(A ⟷ B) = ((A) = (B))› by blast} shows
cartouches in the resulting document, but @{term [source=true] ‹A ⟷ B›}
does not show cartouches in the resulting document.
Are there suggestions to get the resulting document more consistent? Is
there a recommended way to disable printing of delimiting cartouches?
Should I stop using cartouches and start using regular quotes again?
Thanks a lot!
Cornelius
Last updated: Apr 26 2024 at 16:20 UTC