changeset 228 | fe45fbb111c5 |
parent 227 | a00c7721fc3b |
child 229 | abc7f90188af |
--- 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 \<Longrightarrow> even (Suc n)" | oddS: "even n \<Longrightarrow> odd (Suc n)" -*) text {* For this we are going to use the parser: