--- a/src/ZF/IMP/Com.thy Fri Aug 12 11:01:18 1994 +0200
+++ b/src/ZF/IMP/Com.thy Fri Aug 12 11:13:23 1994 +0200
@@ -70,7 +70,8 @@
ori "[| <b0,sigma> -b-> w0; <b1,sigma> -b-> w1 |] \
\ ==> <b0 ori b1,sigma> -b-> (w0 or w1)"
- type_intrs "bexp.intrs @ [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
+ type_intrs "bexp.intrs @ \
+\ [apply_funtype, and_type, or_type, bool_1I, bool_0I, not_type]"
type_elims "[make_elim(evala.dom_subset RS subsetD)]"
@@ -123,6 +124,7 @@
con_defs "[assign_def]"
type_intrs "bexp.intrs @ com.intrs @ [if_type,lam_type,apply_type]"
- type_elims "[make_elim(evala.dom_subset RS subsetD), make_elim(evalb.dom_subset RS subsetD) ]"
+ type_elims "[make_elim(evala.dom_subset RS subsetD), \
+\ make_elim(evalb.dom_subset RS subsetD) ]"
end