ProgTutorial/Package/Ind_Interface.thy
changeset 566 6103b0eadbf2
parent 565 cecd7a941885
child 567 f7c97e64cc2a
--- 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