ProgTutorial/Package/Ind_Interface.thy
changeset 553 c53d74b34123
parent 542 4b96e3c8b33e
child 558 84aef87b348a
--- a/ProgTutorial/Package/Ind_Interface.thy	Sun Dec 15 23:49:05 2013 +0000
+++ b/ProgTutorial/Package/Ind_Interface.thy	Thu Mar 13 17:16:49 2014 +0000
@@ -119,9 +119,9 @@
   parse spec_parser input
 end"
 "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
-     [((even0,\<dots>), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"),
-      ((evenS,\<dots>), \"\\^E\\^Ftoken\\^Eodd n \<Longrightarrow> even (Suc n)\\^E\\^F\\^E\"),
-      ((oddS,\<dots>), \"\\^E\\^Ftoken\\^Eeven n \<Longrightarrow> odd (Suc n)\\^E\\^F\\^E\")]), [])"}
+     [((even0,\<dots>), \<dots>),
+      ((evenS,\<dots>), \<dots>),
+      ((oddS,\<dots>), \<dots>)]), [])"}
 
   then we get back the specifications of the predicates (with type and syntax annotations), 
   and specifications of the introduction rules. This is all the information we