diff -r cecd7a941885 -r 6103b0eadbf2 ProgTutorial/Package/Ind_Interface.thy --- a/ProgTutorial/Package/Ind_Interface.thy Tue May 14 17:10:47 2019 +0200 +++ b/ProgTutorial/Package/Ind_Interface.thy Tue May 14 17:45:13 2019 +0200 @@ -119,9 +119,9 @@ parse spec_parser input end" "(([(even, NONE, NoSyn), (odd, NONE, NoSyn)], - [((even0,\), \), - ((evenS,\), \), - ((oddS,\), \)]), [])"} + [((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