# HG changeset patch
# User paulson
# Date 819635620 -3600
# Node ID 04eabfa73d83ab471f1f65fe9a44f4dc8e8d5fed
# Parent  a6a034a47a71ed0c947e8225c8791ed8b116331a
Added line breaks and other cosmetic changes

diff -r a6a034a47a71 -r 04eabfa73d83 src/ZF/IMP/Com.ML
--- a/src/ZF/IMP/Com.ML	Fri Dec 22 12:25:20 1995 +0100
+++ b/src/ZF/IMP/Com.ML	Fri Dec 22 13:33:40 1995 +0100
@@ -10,15 +10,16 @@
 	"!!n. [| sigma:loc -> nat; n:nat |] ==> sigma[n/x] : loc -> nat"
     (fn _ => [ fast_tac (ZF_cs addIs [apply_type,lam_type,if_type]) 1 ]);
 
-val type_cs = ZF_cs addSEs [make_elim(evala.dom_subset RS subsetD),
-                            make_elim(evalb.dom_subset RS subsetD),
-                            make_elim(evalc.dom_subset RS subsetD)];
+val type_cs = ZF_cs addSDs [evala.dom_subset RS subsetD,
+                            evalb.dom_subset RS subsetD,
+                            evalc.dom_subset RS subsetD];
 
 (**********     type_intrs for evala     **********)
 
 val evala_type_intrs = 
  map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
- ["!!a.<a,sigma> -a-> n ==> a:aexp","!!a.<a,sigma> -a-> n ==> sigma:loc->nat",
+ ["!!a.<a,sigma> -a-> n ==> a:aexp",
+  "!!a.<a,sigma> -a-> n ==> sigma:loc->nat",
   "!!a.<a,sigma> -a-> n ==> n:nat"];
 
 
@@ -26,7 +27,8 @@
 
 val evalb_type_intrs = 
  map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
- ["!!b.<b,sigma> -b-> w ==> b:bexp","!!b.<b,sigma> -b-> w ==> sigma:loc->nat",
+ ["!!b.<b,sigma> -b-> w ==> b:bexp",
+  "!!b.<b,sigma> -b-> w ==> sigma:loc->nat",
   "!!b.<b,sigma> -b-> w ==> w:bool"];