Email Gateway (Nov 14 2024 at 10:46): Email Gateway (Nov 14 2024 at 10:46):From: Stepan Holub <cl-isabelle-users@lists.cam.ac.uk>
Hello,
I am encountering an unexpected and unpleasant behavior of tag "invisible".
As a minimal example consider code:
lemma A ==> A
proof-
assume A
then show A
by simp
qed
I want to see:
lemma A ==> A
proof-
assume A
then show A
qed
However, writing
lemma A ==> A
proof-
assume A
then show A
by simp ✐‹tag invisible›
qed
one gets in the output document the following:
lemma A ==> A
proof-
assume A
then show Aqed
Is this intended? Is there a way to put the "qed" on the new line?
Thanks.
Stepan
Last updated: Jan 04 2025 at 20:18 UTC