removed superfluous type_intrs in datatype com.
authornipkow
Wed, 26 Oct 1994 17:41:40 +0100
changeset 658 368aa02631d8
parent 657 2b16819fbd71
child 659 95ed2ccb4438
removed superfluous type_intrs in datatype com.
src/ZF/IMP/Com.thy
--- a/src/ZF/IMP/Com.thy	Wed Oct 26 15:20:55 1994 +0100
+++ b/src/ZF/IMP/Com.thy	Wed Oct 26 17:41:40 1994 +0100
@@ -84,7 +84,6 @@
         | semic ("c0:com", "c1:com")		("_; _"  [60, 60] 10)
 	| while ("b:bexp", "c:com")		("while _ do _"  60)
 	| ifc   ("b:bexp", "c0:com", "c1:com")	("ifc _ then _ else _"  60)
-  type_intrs "aexp.intrs"
 
 (*Constructor ";" has low precedence to avoid syntactic ambiguities
   with [| m: nat; x: loc; ... |] ==> ...  It usually will need parentheses.*)