Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] document preparation / hiding attributes

view this post on Zulip Email Gateway (Aug 18 2022 at 16:04):

From: Matthias Schmalz <Matthias.Schmalz@inf.ethz.ch>
-----BEGIN PGP SIGNED MESSAGE-----
Hash: SHA1

Dear all,

I wonder whether there is a way to hide attributes for document
preparation similar as it is possible to hide proofs.
For example, in

lemma foo [simp]: ...
proof
...
qed

I know how to make a document version without "proof ... qed", but I do
not know how to make a version without "[simp]".
(Of course, I could use (<) and (>), but that would be hard to
maintain.)

Thanks in advance,

Matthias
-----BEGIN PGP SIGNATURE-----
Version: GnuPG v1.4.6 (GNU/Linux)
Comment: Using GnuPG with Mozilla - http://enigmail.mozdev.org

iD8DBQFMjhZUczhznXSdWggRAp6RAJ0Qa+V9o/9IiqfGTNZ/PrUJI2aDHgCfZij1
97GBvByzT+PnqBVk4XbRvm4=
=qB6p
-----END PGP SIGNATURE-----

view this post on Zulip Email Gateway (Aug 18 2022 at 16:04):

From: Makarius <makarius@sketis.net>
I would say (<) ... (>) is the proper way for that, although one needs
some care of not mixing it with the document "tag" system for changing the
LaTeX output, such as %invisible.

You can also play trick with embedded "-- {* ... *}" but that is a
different story. (Christian Urban is the uberhacker here.)

Makarius

Last updated: Apr 26 2024 at 20:16 UTC