diff -r 444bc9f17cfc -r 3d27d77c351f ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Tue Nov 24 22:55:44 2009 +0100
+++ b/ProgTutorial/Essential.thy	Wed Nov 25 21:00:31 2009 +0100
@@ -1885,8 +1885,12 @@
   @{text ">"}~@{thm (my_strip_allq2 x' x'') style_test}
   \end{isabelle}
 
-  Such theorem styles allow one to print out theorems in documents formatted to
-  ones heart content. Next we explain theorem attributes, which is another
+  Such styles allow one to print out theorems in documents formatted to 
+  ones heart content. The styles can also be used in the document 
+  antiquotations @{text "@{prop ...}"}, @{text "@{term_type ...}"}
+  and @{text "@{typeof ...}"}.
+
+  Next we explain theorem attributes, which is another
   mechanism for dealing with theorems.
 
   \begin{readmore}