ProgTutorial/Parsing.thy
changeset 211 d5accbc67e1b
parent 207 d3cd633e8240
child 218 7ff7325e3b4e
child 220 fbcb89d84ba6
--- 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)