--- a/CookBook/FirstSteps.thy	Fri Feb 27 15:59:38 2009 +0000
+++ b/CookBook/FirstSteps.thy	Sat Feb 28 14:18:02 2009 +0000
@@ -962,8 +962,8 @@
   is meant to be more than just for testing purposes! Here it is only used 
   to illustrate matters. We will show later how to store data properly without 
   using references. The function @{ML Thm.declaration_attribute} expects us to 
-  provide two functions that add and delete theorems from this list. At
-  the moment we use the two functions:
+  provide two functions that add and delete theorems from this list. 
+  For this we use the two functions:
 *}
 
 ML{*fun my_thms_add thm ctxt =
@@ -1114,10 +1114,10 @@
   data.
   \end{readmore}
 
-  What are: 
+  (FIXME What are: 
 
   @{text "theory_attributes"}
-  @{text "proof_attributes"}
+  @{text "proof_attributes"})
 
 
   \begin{readmore}
@@ -1126,7 +1126,7 @@
 *}
 
 
-section {* Theories, Contexts and Local Theories *}
+section {* Theories, Contexts and Local Theories (TBD) *}
 
 text {*
   (FIXME: expand)
@@ -1148,7 +1148,7 @@
 
 
 
-section {* Storing Theorems\label{sec:storing} *}
+section {* Storing Theorems\label{sec:storing} (TBD) *}
 
 text {* @{ML PureThy.add_thms_dynamic} *}
 
@@ -1178,7 +1178,13 @@
 thm foo_def
 (*>*)
 
-section {* Misc *}
+section {* Pretty-Printing (TBD) *}
+
+text {*
+  @{ML Pretty.big_list}
+*}
+
+section {* Misc (TBD) *}
 
 ML {*DatatypePackage.get_datatype @{theory} "List.list"*}