--- a/ProgTutorial/Parsing.thy Thu Mar 26 19:00:51 2009 +0000
+++ b/ProgTutorial/Parsing.thy Fri Mar 27 12:49:28 2009 +0000
@@ -752,7 +752,7 @@
section {* New Commands and Keyword Files\label{sec:newcommand} *}
text {*
- (FIXME: update to the right command setup --- is this still needed)
+ (FIXME: update to the right command setup --- is this still needed?)
Often new commands, for example for providing new definitional principles,
need to be implemented. While this is not difficult on the ML-level,
@@ -1008,7 +1008,7 @@
(FIXME read a name and show how to store theorems)
*}
-section {* Methods *}
+section {* Methods (TBD) *}
text {*
(FIXME: maybe move to after the tactic section)