diff -r a00c7721fc3b -r fe45fbb111c5 ProgTutorial/Parsing.thy --- a/ProgTutorial/Parsing.thy Thu Apr 02 12:19:11 2009 +0100 +++ b/ProgTutorial/Parsing.thy Fri Apr 03 07:55:07 2009 +0100 @@ -618,14 +618,12 @@ for inductive predicates of the form: *} -(* simple_inductive even and odd where even0: "even 0" | evenS: "odd n \ even (Suc n)" | oddS: "even n \ odd (Suc n)" -*) text {* For this we are going to use the parser: