Added line breaks and other cosmetic changes
authorpaulson
Fri Dec 22 13:33:40 1995 +0100 (1995-12-22)
changeset 142004eabfa73d83
parent 1419 a6a034a47a71
child 1421 1471e85624a7
Added line breaks and other cosmetic changes
src/ZF/IMP/Com.ML
     1.1 --- a/src/ZF/IMP/Com.ML	Fri Dec 22 12:25:20 1995 +0100
     1.2 +++ b/src/ZF/IMP/Com.ML	Fri Dec 22 13:33:40 1995 +0100
     1.3 @@ -10,15 +10,16 @@
     1.4  	"!!n. [| sigma:loc -> nat; n:nat |] ==> sigma[n/x] : loc -> nat"
     1.5      (fn _ => [ fast_tac (ZF_cs addIs [apply_type,lam_type,if_type]) 1 ]);
     1.6  
     1.7 -val type_cs = ZF_cs addSEs [make_elim(evala.dom_subset RS subsetD),
     1.8 -                            make_elim(evalb.dom_subset RS subsetD),
     1.9 -                            make_elim(evalc.dom_subset RS subsetD)];
    1.10 +val type_cs = ZF_cs addSDs [evala.dom_subset RS subsetD,
    1.11 +                            evalb.dom_subset RS subsetD,
    1.12 +                            evalc.dom_subset RS subsetD];
    1.13  
    1.14  (**********     type_intrs for evala     **********)
    1.15  
    1.16  val evala_type_intrs = 
    1.17   map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
    1.18 - ["!!a.<a,sigma> -a-> n ==> a:aexp","!!a.<a,sigma> -a-> n ==> sigma:loc->nat",
    1.19 + ["!!a.<a,sigma> -a-> n ==> a:aexp",
    1.20 +  "!!a.<a,sigma> -a-> n ==> sigma:loc->nat",
    1.21    "!!a.<a,sigma> -a-> n ==> n:nat"];
    1.22  
    1.23  
    1.24 @@ -26,7 +27,8 @@
    1.25  
    1.26  val evalb_type_intrs = 
    1.27   map (fn s => prove_goal Com.thy s (fn _ => [(fast_tac type_cs 1)]))
    1.28 - ["!!b.<b,sigma> -b-> w ==> b:bexp","!!b.<b,sigma> -b-> w ==> sigma:loc->nat",
    1.29 + ["!!b.<b,sigma> -b-> w ==> b:bexp",
    1.30 +  "!!b.<b,sigma> -b-> w ==> sigma:loc->nat",
    1.31    "!!b.<b,sigma> -b-> w ==> w:bool"];
    1.32  
    1.33