fixed some weak elim rules

--- a/src/ZF/Cardinal.ML	Wed Jun 28 10:56:01 2000 +0200
+++ b/src/ZF/Cardinal.ML	Wed Jun 28 10:56:34 2000 +0200
@@ -449,8 +449,8 @@
 by (rtac CollectI 1);
 (*Proving it's in the function space A->B*)
 by (rtac (if_type RS lam_type) 1);
-by (blast_tac (claset() addEs [apply_funtype RS consE]) 1);
-by (blast_tac (claset() addSEs [mem_irrefl] addEs [apply_funtype RS consE]) 1);
+by (blast_tac (claset() addDs [apply_funtype]) 1);
+by (blast_tac (claset() addSEs [mem_irrefl] addDs [apply_funtype]) 1);
 (*Proving it's injective*)
 by (Asm_simp_tac 1);
 by (Blast_tac 1);
@@ -481,7 +481,7 @@
 by (rtac iffI 1);
 by (asm_simp_tac (simpset() addsimps [eqpoll_refl]) 2);
 by (blast_tac (claset() addIs [nat_lepoll_imp_le, le_anti_sym] 
-                    addSEs [eqpollE]) 1);
+                        addSEs [eqpollE]) 1);
 qed "nat_eqpoll_iff";
 
 (*The object of all this work: every natural number is a (finite) cardinal*)

--- a/src/ZF/Finite.ML	Wed Jun 28 10:56:01 2000 +0200
+++ b/src/ZF/Finite.ML	Wed Jun 28 10:56:34 2000 +0200
@@ -177,8 +177,7 @@
 \     <-> f : FiniteFun(A,B) & (ALL x:domain(f). P(f`x))";
 by Auto_tac;
 by (blast_tac (claset() addIs [impOfSubs FiniteFun_mono]) 1);
-by (blast_tac (claset() addDs [FiniteFun_is_fun]
-                        addEs [Pair_mem_PiE]) 1);
+by (blast_tac (claset() addDs [Pair_mem_PiD, FiniteFun_is_fun]) 1);
 by (res_inst_tac [("A1", "domain(f)")]
     (subset_refl RSN(2, FiniteFun_mono) RS subsetD) 1);
 by (fast_tac (claset() addDs

--- a/src/ZF/OrderArith.ML	Wed Jun 28 10:56:01 2000 +0200
+++ b/src/ZF/OrderArith.ML	Wed Jun 28 10:56:34 2000 +0200
@@ -254,7 +254,7 @@
 \         (lam z:A. <x,z>) : ord_iso(A, r, {x}*A, rmult({x}, xr, A, r))";
 by (resolve_tac [singleton_prod_bij RS ord_isoI] 1);
 by (Asm_simp_tac 1);
-by (blast_tac (claset() addEs [well_ord_is_wf RS wf_on_not_refl RS notE]) 1);
+by (blast_tac (claset() addDs [well_ord_is_wf RS wf_on_not_refl]) 1);
 qed "singleton_prod_ord_iso";
 
 (*Here we build a complicated function term, then simplify it using
@@ -281,10 +281,8 @@
 by (resolve_tac [prod_sum_singleton_bij RS ord_isoI] 1);
 by (asm_simp_tac
     (simpset() addsimps [pred_iff, well_ord_is_wf RS wf_on_not_refl]) 1);
-by (Asm_simp_tac 1);
-by (REPEAT_FIRST (eresolve_tac [SigmaE, sumE, predE]));
-by (ALLGOALS Asm_simp_tac);
-by (ALLGOALS (blast_tac (claset() addEs [well_ord_is_wf RS wf_on_asym])));
+by (auto_tac (claset() addSEs [well_ord_is_wf RS wf_on_asym, predE], 
+	      simpset()));
 qed "prod_sum_singleton_ord_iso";
 
 (** Distributive law **)

--- a/src/ZF/OrderType.ML	Wed Jun 28 10:56:01 2000 +0200
+++ b/src/ZF/OrderType.ML	Wed Jun 28 10:56:34 2000 +0200
@@ -510,14 +510,14 @@
 \     i ++ (UN x:A. j(x)) = (UN x:A. i++j(x))";
 by (blast_tac (claset() addIs prems @ [ltI, Ord_UN, Ord_oadd, 
 				       lt_oadd1 RS ltD, oadd_lt_mono2 RS ltD]
-                        addSEs [ltE, ltI RS lt_oadd_disj RS disjE]) 1);
+                        addSEs [ltE] addSDs [ltI RS lt_oadd_disj]) 1);
 qed "oadd_UN";
 
 Goal "[| Ord(i);  Limit(j) |] ==> i++j = (UN k:j. i++k)";
 by (forward_tac [Limit_has_0 RS ltD] 1);
 by (asm_simp_tac (simpset() addsimps [Limit_is_Ord RS Ord_in_Ord,
-                                  oadd_UN RS sym, Union_eq_UN RS sym, 
-                                  Limit_Union_eq]) 1);
+				      oadd_UN RS sym, Union_eq_UN RS sym, 
+				      Limit_Union_eq]) 1);
 qed "oadd_Limit";
 
 (** Order/monotonicity properties of ordinal addition **)

--- a/src/ZF/Perm.ML	Wed Jun 28 10:56:01 2000 +0200
+++ b/src/ZF/Perm.ML	Wed Jun 28 10:56:34 2000 +0200
@@ -57,8 +57,7 @@
 (*Good for dealing with sets of pairs, but a bit ugly in use [used in AC]*)
 Goalw [inj_def]
     "[| <a,b>:f;  <c,b>:f;  f: inj(A,B) |] ==> a=c";
-by (REPEAT (eresolve_tac [asm_rl, Pair_mem_PiE, CollectE] 1));
-by (Blast_tac 1);
+by (blast_tac (claset() addDs [Pair_mem_PiD]) 1);
 qed "inj_equality";
 
 Goalw [inj_def] "[| f:inj(A,B);  a:A;  b:A;  f`a=f`b |] ==> a=b";

--- a/src/ZF/Univ.ML	Wed Jun 28 10:56:01 2000 +0200
+++ b/src/ZF/Univ.ML	Wed Jun 28 10:56:34 2000 +0200
@@ -193,9 +193,10 @@
 qed "Limit_VfromI";
 
 val prems = Goal
-    "[| a: Vfrom(A,i);  Limit(i);               \
+    "[| a: Vfrom(A,i);  ~R ==> Limit(i);               \
 \       !!x. [| x<i;  a: Vfrom(A,x) |] ==> R    \
 \    |] ==> R";
+by (rtac classical 1);
 by (rtac (Limit_Vfrom_eq RS equalityD1 RS subsetD RS UN_E) 1);
 by (REPEAT (ares_tac (prems @ [ltI, Limit_is_Ord]) 1));
 qed "Limit_VfromE";
@@ -209,8 +210,8 @@
 by (etac (limiti RS Limit_has_succ) 1);
 qed "singleton_in_VLimit";
 
-val Vfrom_UnI1 = Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD)
-and Vfrom_UnI2 = Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD);
+bind_thm ("Vfrom_UnI1", Un_upper1 RS (subset_refl RS Vfrom_mono RS subsetD));
+bind_thm ("Vfrom_UnI2", Un_upper2 RS (subset_refl RS Vfrom_mono RS subsetD));
 
 (*Hard work is finding a single j:i such that {a,b}<=Vfrom(A,j)*)
 val [aprem,bprem,limiti] = goal Univ.thy
@@ -403,7 +404,7 @@
 
 Goal "[| a: Vfrom(A,i);  Limit(i);  Transset(A) |] ==> Pow(a) : Vfrom(A,i)";
 by (blast_tac (claset() addEs [Limit_VfromE]
-		        addIs [Limit_has_succ, Pow_in_Vfrom, Limit_VfromI]) 1);
+	                addIs [Limit_has_succ, Pow_in_Vfrom, Limit_VfromI]) 1);
 qed "Pow_in_VLimit";
 
 

--- a/src/ZF/WF.ML	Wed Jun 28 10:56:01 2000 +0200
+++ b/src/ZF/WF.ML	Wed Jun 28 10:56:34 2000 +0200
@@ -17,8 +17,6 @@
 a mess.
 *)
 
-open WF;
-
 
 (*** Well-founded relations ***)
 
@@ -159,15 +157,9 @@
 by (Blast_tac 1);
 qed_spec_mp "wf_on_not_sym";
 
-(* [| wf[A](r);  <a,b> : r;  a:A;  b:A;  ~P ==> <b,a> : r |] ==> P *)
-bind_thm ("wf_on_asym", wf_on_not_sym RS swap);
-
-val prems =
-Goal "[| wf[A](r);  <a,b>:r;  ~P ==> <b,a>:r;  a:A;  b:A |] ==> P";
-by (rtac ccontr 1);
-by (rtac (wf_on_not_sym RS notE) 1);
-by (DEPTH_SOLVE (ares_tac prems 1));
-qed "wf_on_asym";
+(* [| wf[A](r); ~Z ==> <a,b> : r;
+      <b,a> ~: r ==> Z; ~Z ==> a : A; ~Z ==> b : A |] ==> Z *)
+bind_thm ("wf_on_asym", permute_prems 1 2 (cla_make_elim wf_on_not_sym));
 
 (*Needed to prove well_ordI.  Could also reason that wf[A](r) means
   wf(r Int A*A);  thus wf( (r Int A*A)^+ ) and use wf_not_refl *)

--- a/src/ZF/func.ML	Wed Jun 28 10:56:01 2000 +0200
+++ b/src/ZF/func.ML	Wed Jun 28 10:56:34 2000 +0200
@@ -142,14 +142,9 @@
 by (assume_tac 1);
 qed "range_type";
 
-val prems = Goal
-    "[| <a,b>: f;  f: Pi(A,B);       \
-\       [| a:A;  b:B(a);  f`a = b |] ==> P  \
-\    |] ==> P";
-by (cut_facts_tac prems 1);
-by (resolve_tac prems 1);
-by (REPEAT (eresolve_tac [asm_rl,domain_type,range_type,apply_equality] 1));
-qed "Pair_mem_PiE";
+Goal "[| <a,b>: f;  f: Pi(A,B) |] ==> a:A & b:B(a) & f`a = b";
+by (blast_tac (claset() addIs [domain_type, range_type, apply_equality]) 1);
+qed "Pair_mem_PiD";
 
 (*** Lambda Abstraction ***)