--- a/CookBook/Recipes/Antiquotes.thy Thu Jan 08 22:47:15 2009 +0000
+++ b/CookBook/Recipes/Antiquotes.thy Sat Jan 10 12:57:48 2009 +0000
@@ -4,6 +4,8 @@
begin
+
+
section {* Useful Document Antiquotations *}
text {*
@@ -14,9 +16,10 @@
Document antiquotations can be used for ensuring consistent type-setting of
various entities in a document. They can also be used for sophisticated
- \LaTeX-hacking.
+ \LaTeX-hacking. If you type @{text "Ctrl-c Ctrl-a h A"} inside ProofGeneral, you
+ obtain a list of all available document antiquotations and their options.
- Below we give the code for two antiquotations that can be used to typeset
+ Below we give the code for two additional antiquotations that can be used to typeset
ML-code and also to check whether the given code actually compiles. This
provides a sanity check for the code and also allows one to keep documents
in sync with other code, for example Isabelle.