--- a/CookBook/FirstSteps.thy	Wed Mar 18 18:32:31 2009 +0100
+++ b/CookBook/FirstSteps.thy	Wed Mar 18 23:52:51 2009 +0100
@@ -178,6 +178,10 @@
 ML{*fun str_of_thms ctxt thms =  
   commas (map (str_of_thm ctxt) thms)*}
 
+text {*
+(FIXME @{ML Toplevel.debug} @{ML Toplevel.profiling} @{ML Toplevel.debug})
+*}
+
 section {* Combinators\label{sec:combinators} *}
 
 text {*

--- a/CookBook/Parsing.thy	Wed Mar 18 18:32:31 2009 +0100
+++ b/CookBook/Parsing.thy	Wed Mar 18 23:52:51 2009 +0100
@@ -347,6 +347,8 @@
 section {* Parsing Theory Syntax *}
 
 text {*
+  (FIXME: context parser)
+
   Most of the time, however, Isabelle developers have to deal with parsing
   tokens, not strings.  These token parsers have the type:
 *}
@@ -712,6 +714,8 @@
 section {* New Commands and Keyword Files\label{sec:newcommand} *}
 
 text {*
+  (FIXME: update to the right command setup)
+
   Often new commands, for example for providing new definitional principles,
   need to be implemented. While this is not difficult on the ML-level,
   new commands, in order to be useful, need to be recognised by

--- a/CookBook/Recipes/Antiquotes.thy	Wed Mar 18 18:32:31 2009 +0100
+++ b/CookBook/Recipes/Antiquotes.thy	Wed Mar 18 23:52:51 2009 +0100
@@ -7,6 +7,8 @@
 section {* Useful Document Antiquotations *}
 
 text {*
+  (FIXME: update to to new antiquotation setup)
+
   {\bf Problem:} 
   How to keep your ML-code inside a document synchronised with the actual code?\smallskip
 

Binary file cookbook.pdf has changed