--- a/CookBook/Package/Ind_Interface.thy Sat Mar 14 00:48:22 2009 +0100
+++ b/CookBook/Package/Ind_Interface.thy Mon Mar 16 00:12:32 2009 +0100
@@ -360,6 +360,8 @@
The definition of the transitive closure should look as follows:
*}
+ML {* SpecParse.opt_thm_name *}
+
text {*
A proposition can be parsed using the function @{ML prop in OuterParse}.
@@ -377,7 +379,7 @@
\begin{table}
@{ML "opt_thm_name:
- string -> token list -> Attrib.binding * token list" in SpecParse}
+ string -> Attrib.binding parser" in SpecParse}
\end{table}
We now have all the necessary tools to write the parser for our