--- 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