CookBook/Parsing.thy
changeset 188 8939b8fd8603
parent 186 371e4375c994
--- 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