ProgTutorial/Parsing.thy
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: