src/ZF/Resid/SubUnion.ML

-(*  Title: 	SubUnion.ML
+(*  Title:      SubUnion.ML
     ID:         $Id$
-    Author: 	Ole Rasmussen
+    Author:     Ole Rasmussen
     Copyright   1995  University of Cambridge
     Logic Image: ZF
 *)
 
 open SubUnion;

 by (simp_tac (rank_ss addsimps redexes.con_defs)  1);
 val union_App = result();
 
 val union_ss = redexes_ss addsimps 
                 (Ssub.intrs@bool_simps@bool_typechecks@
-		 [e-mail]@
-		 [or_1 RSN (3,or_commute RS trans),
-		  or_0 RSN (3,or_commute RS trans),
-		  union_App,union_Fun,union_Var,compD2,compD1,regD]);
+                 [e-mail]@
+                 [or_1 RSN (3,or_commute RS trans),
+                  or_0 RSN (3,or_commute RS trans),
+                  union_App,union_Fun,union_Var,compD2,compD1,regD]);
 
 val union_cs = (ZF_cs addIs Scomp.intrs addSEs 
-		[Sreg.mk_cases redexes.con_defs "regular(App(b,f,a))",
-		 Sreg.mk_cases redexes.con_defs "regular(Fun(b))",
-		 Sreg.mk_cases redexes.con_defs "regular(Var(b))",
-		 Scomp.mk_cases redexes.con_defs "Fun(u) ~ Fun(t)",
-		 Scomp.mk_cases redexes.con_defs "u ~ Fun(t)",
-		 Scomp.mk_cases redexes.con_defs "u ~ Var(n)",
-		 Scomp.mk_cases redexes.con_defs "u ~ App(b,t,a)",
-		 Scomp.mk_cases redexes.con_defs "Fun(t) ~ v",
-		 Scomp.mk_cases redexes.con_defs "App(b,f,a) ~ v",
-		 Scomp.mk_cases redexes.con_defs "Var(n) ~ u"
-		 ]);
+                [Sreg.mk_cases redexes.con_defs "regular(App(b,f,a))",
+                 Sreg.mk_cases redexes.con_defs "regular(Fun(b))",
+                 Sreg.mk_cases redexes.con_defs "regular(Var(b))",
+                 Scomp.mk_cases redexes.con_defs "Fun(u) ~ Fun(t)",
+                 Scomp.mk_cases redexes.con_defs "u ~ Fun(t)",
+                 Scomp.mk_cases redexes.con_defs "u ~ Var(n)",
+                 Scomp.mk_cases redexes.con_defs "u ~ App(b,t,a)",
+                 Scomp.mk_cases redexes.con_defs "Fun(t) ~ v",
+                 Scomp.mk_cases redexes.con_defs "App(b,f,a) ~ v",
+                 Scomp.mk_cases redexes.con_defs "Var(n) ~ u"
+                 ]);
 
 
 
 (* ------------------------------------------------------------------------- *)
 (*    comp proofs                                                            *)

 by (ALLGOALS(fast_tac union_cs));
 val comp_refl = result();
 
 goal SubUnion.thy 
     "!!u.u ~ v ==> v ~ u";
-by (eresolve_tac [comp_induct] 1);
+by (etac comp_induct 1);
 by (ALLGOALS(fast_tac union_cs));
 val comp_sym = result();
 
 goal SubUnion.thy 
     "u ~ v <-> v ~ u";

 val comp_sym_iff = result();
 
 
 goal SubUnion.thy 
     "!!u.u ~ v ==> ALL w.v ~ w-->u ~ w";
-by (eresolve_tac [comp_induct] 1);
+by (etac comp_induct 1);
 by (ALLGOALS(fast_tac union_cs));
 val comp_trans1 = result();
 
 val comp_trans = comp_trans1 RS spec RS mp;
 

 val sub_induct = standard
     (Ssub.mutual_induct RS spec RS spec RSN (2,rev_mp));
 
 goal SubUnion.thy 
     "!!u.u ~ v ==> u <== (u un v)";
-by (eresolve_tac [comp_induct] 1);
-by (eresolve_tac [boolE] 3);
+by (etac comp_induct 1);
+by (etac boolE 3);
 by (ALLGOALS(asm_full_simp_tac union_ss));
 val union_l = result();
 
 goal SubUnion.thy 
     "!!u.u ~ v ==> v <== (u un v)";
-by (eresolve_tac [comp_induct] 1);
+by (etac comp_induct 1);
 by (eres_inst_tac [("c","b2")] boolE 3);
 by (ALLGOALS(asm_full_simp_tac union_ss));
 val union_r = result();
 
 goal SubUnion.thy 
     "!!u.u ~ v ==> u un v = v un u";
-by (eresolve_tac [comp_induct] 1);
+by (etac comp_induct 1);
 by (ALLGOALS(asm_simp_tac (union_ss addsimps [or_commute])));
 val union_sym = result();
 
 (* ------------------------------------------------------------------------- *)
 (*      regular proofs                                                       *)
 (* ------------------------------------------------------------------------- *)
 
 goal SubUnion.thy 
     "!!u.u ~ v ==> regular(u)-->regular(v)-->regular(u un v)";
-by (eresolve_tac [comp_induct] 1);
+by (etac comp_induct 1);
 by (ALLGOALS(asm_full_simp_tac
-	     (union_ss setloop(SELECT_GOAL (safe_tac union_cs)))));
+             (union_ss setloop(SELECT_GOAL (safe_tac union_cs)))));
 by (dres_inst_tac [("psi", "regular(Fun(?u) un ?v)")] asm_rl 1);
 by (asm_full_simp_tac union_ss 1);
 val union_preserve_regular = result();