--- a/ProgTutorial/Intro.thy Sun Nov 15 13:47:31 2009 +0100
+++ b/ProgTutorial/Intro.thy Tue Nov 17 18:40:11 2009 +0100
@@ -194,6 +194,7 @@
\item @{text t}, @{text u}, @{text trm} for (raw) terms; ML-type: @{ML_type term}
\item @{text ct}, @{text cu} for certified terms; ML-type: @{ML_type cterm}
\item @{text "ty"}, @{text T}, @{text U} for (raw) types; ML-type: @{ML_type typ}
+ \item @{text "S"} for sorts; ML-type: @{ML_type sort}
\item @{text th}, @{text thm} for theorems; ML-type: @{ML_type thm}
\item @{text "foo_tac"} for tactics; ML-type: @{ML_type tactic}
\item @{text thy} for theories; ML-type: @{ML_type theory}
@@ -226,6 +227,9 @@
and helped with recipe \ref{rec:timing}. Parts of section \ref{sec:storing}
are by him.
+ \item {\bf Lukas Bulwahn} made me aware of the problems with recursive
+ parsers.
+
\item {\bf Jeremy Dawson} wrote the first version of the chapter
about parsing.
@@ -255,6 +259,4 @@
\input{pversion}
*}
-
-
end