diff -r bbb2d5f1d58d -r 14c3dd5ee2ad CookBook/FirstSteps.thy
--- a/CookBook/FirstSteps.thy	Wed Jan 14 18:30:41 2009 +0000
+++ b/CookBook/FirstSteps.thy	Wed Jan 14 21:46:04 2009 +0000
@@ -157,10 +157,11 @@
   map #name (Net.entries rules)
 end" "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
 
-  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}.
+  The second example extracts the theorem names that are stored in a simpset.
+  For this 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
   avoid explicit bindings for theorems such as
@@ -185,8 +186,9 @@
   One way to construct terms of Isabelle on the ML-level is by using the antiquotation 
   \mbox{@{text "@{term \<dots>}"}}. For example
 
-  @{ML_response [display] "@{term \"(a::nat) + b = c\"}" 
-                          "Const (\"op =\", \<dots>)  $ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
+  @{ML_response [display] 
+    "@{term \"(a::nat) + b = c\"}" 
+    "Const (\"op =\", \<dots>) $ (Const (\"HOL.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
 
   This will show the term @{term "(a::nat) + b = c"}, but printed using the internal
   representation of this term. This internal representation corresponds to the