--- a/ProgTutorial/Parsing.thy Sat May 30 23:58:05 2009 +0200
+++ b/ProgTutorial/Parsing.thy Sun May 31 00:39:17 2009 +0200
@@ -288,7 +288,6 @@
where the function @{ML [index] not_eof in Symbol} ensures that we do not read beyond the
end of the input string (i.e.~stopper symbol).
- \indexdef{unless@ {\tt\slshape{unless}}}{in {\tt\slshape Scan}}
The function @{ML "Scan.unless p q" for p q} takes two parsers: if the first one can
parse the input, then the whole parser fails; if not, then the second is tried. Therefore