diff -r 82c482467d75 -r c53d74b34123 ProgTutorial/Package/Ind_Interface.thy --- 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,\), \"\\^E\\^Ftoken\\^Eeven 0\\^E\\^F\\^E\"), - ((evenS,\), \"\\^E\\^Ftoken\\^Eodd n \ even (Suc n)\\^E\\^F\\^E\"), - ((oddS,\), \"\\^E\\^Ftoken\\^Eeven n \ odd (Suc n)\\^E\\^F\\^E\")]), [])"} + [((even0,\), \), + ((evenS,\), \), + ((oddS,\), \)]), [])"} 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