# HG changeset patch # User griff # Date 1248263977 -7200 # Node ID ee139d9d7ab84a7aa27430e15506c62961c25b92 # Parent e5990cd1b51a226f42e91f329e417e36eef865d2 comment diff -r e5990cd1b51a -r ee139d9d7ab8 ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Wed Jul 22 09:53:35 2009 +0200 +++ b/ProgTutorial/Parsing.thy Wed Jul 22 13:59:37 2009 +0200 @@ -798,7 +798,9 @@ OuterParse.!!! (OuterParse.$$$ "|"))))) [] *} text_raw {* \end{isabelle} - Both parsers accept the same input, but if you look closely, you can notice + Both parsers accept the same input% that's not true: + % spec_parser accepts input that is refuted by spec_parser' + , but if you look closely, you can notice an additional ``tail'' (Lines 8 to 10) in @{ML spec_parser'}. What is the purpose of this additional ``tail''? \end{exercise} diff -r e5990cd1b51a -r ee139d9d7ab8 progtutorial.pdf Binary file progtutorial.pdf has changed