--- a/CookBook/FirstSteps.thy	Mon Feb 23 00:27:27 2009 +0000
+++ b/CookBook/FirstSteps.thy	Mon Feb 23 17:08:15 2009 +0000
@@ -376,12 +376,20 @@
   some data structure and return it. Instead, it is literally
   replaced with the value representing the theory name.
 
-  In a similar way you can use antiquotations to refer to proved theorems:
+  In a similar way you can use antiquotations to refer to proved theorems: 
+  for a single theorem
 
   @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
 
-  and current simpsets. For this we use the function that extracts the 
-  theorem names stored in the simpset.
+  and for more than one
+
+@{ML_response_fake [display,gray] "@{thms conj_ac}" 
+"(?P \<and> ?Q) = (?Q \<and> ?P)
+(?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
+((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}  
+
+  You can also refer to the current simpsets. To illustrate this we use the
+  function that extracts the theorem names stored in a simpset.
 *}
 
 ML{*fun get_thm_names simpset =