--- a/CookBook/FirstSteps.thy	Wed Jan 14 17:47:49 2009 +0000
+++ b/CookBook/FirstSteps.thy	Wed Jan 14 18:30:41 2009 +0000
@@ -150,12 +150,19 @@
   In a similar way you can use antiquotations to refer to theorems or simpsets:
 
   @{ML_response_fake [display] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
-  @{ML_response_fake [display] "@{simpset}" "\<dots>"}
+  @{ML_response_fake [display] 
+"let
+  val ({rules,...},_) = MetaSimplifier.rep_ss @{simpset}
+in
+  map #name (Net.entries rules)
+end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
 
-  (FIXME: what does a simpset look like? It seems to be the same problem
-  as with tokens.)
+  In the second example, the function @{ML rep_ss in MetaSimplifier} returns a record
+  containing information about the simpset. The rules of a simpset are stored in a 
+  discrimination net (a datastructure for fast indexing). From this net we can extract 
+  the entries using the function @{ML Net.entries}.
 
-  While antiquotations have many applications, they were originally introduced to 
+  While antiquotations have many applications, they were originally introduced to
   avoid explicit bindings for theorems such as
 *}
 

Binary file cookbook.pdf has changed