# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1237416771 -3600
# Node ID 8939b8fd8603317f25428723cb37d8558212736b
# Parent  e2e805678fb010dc289ce79ed98ed64da498fe82
added lots of FIXMES

diff -r e2e805678fb0 -r 8939b8fd8603 CookBook/FirstSteps.thy
--- 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 {*
diff -r e2e805678fb0 -r 8939b8fd8603 CookBook/Parsing.thy
--- 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
diff -r e2e805678fb0 -r 8939b8fd8603 CookBook/Recipes/Antiquotes.thy
--- 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
 
diff -r e2e805678fb0 -r 8939b8fd8603 cookbook.pdf
Binary file cookbook.pdf has changed