diff -r 9a6e5e0c4906 -r c8e9a4f97916 CookBook/Recipes/Antiquotes.thy
--- 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.