src/ZF/Resid/SubUnion.ML

--- a/src/ZF/Resid/SubUnion.ML	Mon Sep 29 11:51:09 1997 +0200
+++ b/src/ZF/Resid/SubUnion.ML	Mon Sep 29 11:51:52 1997 +0200
@@ -25,20 +25,20 @@
     "!!u.n:nat==>Var(n) un Var(n)=Var(n)";
 by (Asm_simp_tac 1);
 by (simp_tac (rank_ss addsimps redexes.con_defs)  1);
-val union_Var = result();
+qed "union_Var";
 
 goalw SubUnion.thy [union_def]
     "!!u.[|u:redexes; v:redexes|]==>Fun(u) un Fun(v)=Fun(u un v)";
 by (Asm_simp_tac 1);
 by (simp_tac (rank_ss addsimps redexes.con_defs)  1);
-val union_Fun = result();
+qed "union_Fun";
  
 goalw SubUnion.thy [union_def]
  "!!u.[|b1:bool; b2:bool; u1:redexes; v1:redexes; u2:redexes; v2:redexes|]==> \
 \     App(b1,u1,v1) un App(b2,u2,v2)=App(b1 or b2,u1 un u2,v1 un v2)";
 by (Asm_simp_tac 1);
 by (simp_tac (rank_ss addsimps redexes.con_defs)  1);
-val union_App = result();
+qed "union_App";
 
 Addsimps (Ssub.intrs@bool_typechecks@
 	  [e-mail]@
@@ -68,27 +68,25 @@
 goal SubUnion.thy "!!u.u:redexes ==> u ~ u";
 by (eresolve_tac [redexes.induct] 1);
 by (ALLGOALS Fast_tac);
-val comp_refl = result();
+qed "comp_refl";
 
 goal SubUnion.thy 
     "!!u.u ~ v ==> v ~ u";
 by (etac Scomp.induct 1);
 by (ALLGOALS Fast_tac);
-val comp_sym = result();
+qed "comp_sym";
 
 goal SubUnion.thy 
     "u ~ v <-> v ~ u";
 by (fast_tac (!claset addIs [comp_sym]) 1);
-val comp_sym_iff = result();
+qed "comp_sym_iff";
 
 
 goal SubUnion.thy 
     "!!u.u ~ v ==> ALL w.v ~ w-->u ~ w";
 by (etac Scomp.induct 1);
 by (ALLGOALS Fast_tac);
-val comp_trans1 = result();
-
-val comp_trans = comp_trans1 RS spec RS mp;
+qed_spec_mp "comp_trans";
 
 (* ------------------------------------------------------------------------- *)
 (*   union proofs                                                            *)
@@ -99,20 +97,20 @@
 by (etac Scomp.induct 1);
 by (etac boolE 3);
 by (ALLGOALS Asm_full_simp_tac);
-val union_l = result();
+qed "union_l";
 
 goal SubUnion.thy 
     "!!u.u ~ v ==> v <== (u un v)";
 by (etac Scomp.induct 1);
 by (eres_inst_tac [("c","b2")] boolE 3);
 by (ALLGOALS Asm_full_simp_tac);
-val union_r = result();
+qed "union_r";
 
 goal SubUnion.thy 
     "!!u.u ~ v ==> u un v = v un u";
 by (etac Scomp.induct 1);
 by (ALLGOALS(asm_simp_tac (!simpset addsimps [or_commute])));
-val union_sym = result();
+qed "union_sym";
 
 (* ------------------------------------------------------------------------- *)
 (*      regular proofs                                                       *)
@@ -125,4 +123,4 @@
              (!simpset setloop(SELECT_GOAL (safe_tac (!claset))))));
 by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1);
 by (Asm_full_simp_tac 1);
-val union_preserve_regular = result();
+qed_spec_mp "union_preserve_regular";