--- a/src/ZF/CardinalArith.ML Mon Sep 14 10:18:07 1998 +0200
+++ b/src/ZF/CardinalArith.ML Tue Sep 15 10:40:40 1998 +0200
@@ -21,8 +21,7 @@
by (rtac exI 1);
by (res_inst_tac [("c", "case(Inr, Inl)"), ("d", "case(Inr, Inl)")]
lam_bijective 1);
-by (safe_tac (claset() addSEs [sumE]));
-by (ALLGOALS (Asm_simp_tac));
+by Auto_tac;
qed "sum_commute_eqpoll";
Goalw [cadd_def] "i |+| j = j |+| i";
@@ -272,7 +271,7 @@
by (res_inst_tac [("c", "%<x,y>. if(x=A, Inl(y), Inr(<x,y>))"),
("d", "case(%y. <A,y>, %z. z)")]
lam_bijective 1);
-by (safe_tac (claset() addSEs [sumE]));
+by Safe_tac;
by (ALLGOALS
(asm_simp_tac (simpset() addsimps [succI2, if_type, mem_imp_not_eq])));
qed "prod_succ_eqpoll";
@@ -390,14 +389,12 @@
(** Establishing the well-ordering **)
-Goalw [inj_def]
- "Ord(K) ==> (lam <x,y>:K*K. <x Un y, x, y>) : inj(K*K, K*K*K)";
-by (fast_tac (claset() addss (simpset())
- addIs [lam_type, Un_least_lt RS ltD, ltI]) 1);
+Goalw [inj_def] "Ord(K) ==> (lam <x,y>:K*K. <x Un y, x, y>) : inj(K*K, K*K*K)";
+by (force_tac (claset() addIs [lam_type, Un_least_lt RS ltD, ltI],
+ simpset()) 1);
qed "csquare_lam_inj";
-Goalw [csquare_rel_def]
- "Ord(K) ==> well_ord(K*K, csquare_rel(K))";
+Goalw [csquare_rel_def] "Ord(K) ==> well_ord(K*K, csquare_rel(K))";
by (rtac (csquare_lam_inj RS well_ord_rvimage) 1);
by (REPEAT (ares_tac [well_ord_rmult, well_ord_Memrel] 1));
qed "well_ord_csquare";
@@ -405,22 +402,21 @@
(** Characterising initial segments of the well-ordering **)
Goalw [csquare_rel_def]
- "[| x<K; y<K; z<K |] ==> \
-\ <<x,y>, <z,z>> : csquare_rel(K) --> x le z & y le z";
+ "[| <<x,y>, <z,z>> : csquare_rel(K); x<K; y<K; z<K |] ==> x le z & y le z";
+by (etac rev_mp 1);
by (REPEAT (etac ltE 1));
by (asm_simp_tac (simpset() addsimps [rvimage_iff, rmult_iff, Memrel_iff,
Un_absorb, Un_least_mem_iff, ltD]) 1);
by (safe_tac (claset() addSEs [mem_irrefl]
addSIs [Un_upper1_le, Un_upper2_le]));
by (ALLGOALS (asm_simp_tac (simpset() addsimps [lt_def, succI2, Ord_succ])));
-qed_spec_mp "csquareD";
+qed "csquareD";
Goalw [pred_def]
"z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)";
-by (safe_tac (claset_of ZF.thy addSEs [SigmaE])); (*avoids using succCI,...*)
-by (rtac (csquareD RS conjE) 1);
+by (safe_tac (claset() delrules [SigmaI,succCI])); (*avoids using succCI,...*)
+by (etac (csquareD RS conjE) 1);
by (rewtac lt_def);
-by (assume_tac 4);
by (ALLGOALS Blast_tac);
qed "pred_csquare_subset";
--- a/src/ZF/Order.ML Mon Sep 14 10:18:07 1998 +0200
+++ b/src/ZF/Order.ML Tue Sep 15 10:40:40 1998 +0200
@@ -504,7 +504,7 @@
by (asm_simp_tac
(simpset() addsimps [ord_iso_map_fun RSN (2,apply_equality)]) 1);
by (rewtac ord_iso_map_def);
-by (safe_tac (claset() addSEs [UN_E]));
+by Safe_tac;
by (rtac well_ord_iso_preserving 1 THEN REPEAT_FIRST assume_tac);
qed "ord_iso_map_mono_map";
--- a/src/ZF/OrderArith.ML Mon Sep 14 10:18:07 1998 +0200
+++ b/src/ZF/OrderArith.ML Tue Sep 15 10:40:40 1998 +0200
@@ -83,7 +83,7 @@
by (eres_inst_tac [("r","r"),("a","x")] wf_on_induct 2 THEN assume_tac 2);
by (best_tac (claset() addSEs [raddE, bspec RS mp]) 2);
(*Returning to main part of proof*)
-by (REPEAT_FIRST (eresolve_tac [sumE, ssubst]));
+by Safe_tac;
by (Blast_tac 1);
by (eres_inst_tac [("r","s"),("a","ya")] wf_on_induct 1 THEN assume_tac 1);
by (best_tac (claset() addSEs [raddE, bspec RS mp]) 1);
--- a/src/ZF/upair.ML Mon Sep 14 10:18:07 1998 +0200
+++ b/src/ZF/upair.ML Tue Sep 15 10:40:40 1998 +0200
@@ -223,7 +223,7 @@
(*If it's "undefined", it's zero!*)
qed_goalw "the_0" thy [the_def]
"!!P. ~ (EX! x. P(x)) ==> (THE x. P(x))=0"
- (fn _ => [ (deepen_tac (claset() addSEs [ReplaceE]) 0 1) ]);
+ (fn _ => [ (blast_tac (claset() addSEs [ReplaceE]) 1) ]);
(*** if -- a conditional expression for formulae ***)