--- 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,\<dots>), \<dots>),
- ((evenS,\<dots>), \<dots>),
- ((oddS,\<dots>), \<dots>)]), [])"}
+ [((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