--- 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