# HG changeset patch
# User paulson
# Date 875526964 -7200
# Node ID 39ee3d31cfbc66e591d32e4c4332317c8fff5c93
# Parent  bed0ba7bff2f8bd972b128cbd05610220f393d86
Much tidying including step_tac -> clarify_tac or safe_tac; sometimes
used qed_spec_mp

diff -r bed0ba7bff2f -r 39ee3d31cfbc src/ZF/Arith.ML
--- a/src/ZF/Arith.ML	Mon Sep 29 11:52:25 1997 +0200
+++ b/src/ZF/Arith.ML	Mon Sep 29 11:56:04 1997 +0200
@@ -434,7 +434,7 @@
 goal Arith.thy "!!m. m:nat ==> succ(succ(m)) mod 2 = m mod 2";
 by (subgoal_tac "m mod 2: 2" 1);
 by (asm_simp_tac (!simpset addsimps [mod_less_divisor RS ltD]) 2);
-by (asm_simp_tac (!simpset addsimps [mod_succ] setloop step_tac (!claset)) 1);
+by (asm_simp_tac (!simpset addsimps [mod_succ] setloop Step_tac) 1);
 qed "mod2_succ_succ";
 
 goal Arith.thy "!!m. m:nat ==> (m#+m) mod 2 = 0";
@@ -588,7 +588,7 @@
 by (etac rev_mp 1);
 by (eres_inst_tac [("n","n")] nat_induct 1);
 by (Asm_simp_tac 1);
-by (Step_tac 1);
+by Safe_tac;
 by (asm_full_simp_tac (!simpset addsimps [not_le_iff_lt,nat_into_Ord]) 1);
 by (etac lt_asym 1);
 by (assume_tac 1);
diff -r bed0ba7bff2f -r 39ee3d31cfbc src/ZF/Cardinal.ML
--- a/src/ZF/Cardinal.ML	Mon Sep 29 11:52:25 1997 +0200
+++ b/src/ZF/Cardinal.ML	Mon Sep 29 11:56:04 1997 +0200
@@ -508,7 +508,7 @@
 
 goalw Cardinal.thy [lesspoll_def, lepoll_def, eqpoll_def, bij_def]
       "!!m. [| A lesspoll succ(m); m:nat |] ==> A lepoll m";
-by (step_tac (!claset) 1);
+by (Clarify_tac 1);
 by (blast_tac (!claset addSIs [inj_not_surj_succ]) 1);
 qed "lesspoll_succ_imp_lepoll";
 
diff -r bed0ba7bff2f -r 39ee3d31cfbc src/ZF/CardinalArith.ML
--- a/src/ZF/CardinalArith.ML	Mon Sep 29 11:52:25 1997 +0200
+++ b/src/ZF/CardinalArith.ML	Mon Sep 29 11:56:04 1997 +0200
@@ -403,9 +403,7 @@
 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])));
-val csquareD_lemma = result();
-
-bind_thm ("csquareD", csquareD_lemma RS mp);
+qed_spec_mp "csquareD";
 
 goalw CardinalArith.thy [pred_def]
  "!!K. z<K ==> pred(K*K, <z,z>, csquare_rel(K)) <= succ(z)*succ(z)";
@@ -713,7 +711,7 @@
     "!!n. n: nat ==> ALL A. A eqpoll n --> A : Fin(A)";
 by (etac nat_induct 1);
 by (simp_tac (!simpset addsimps (eqpoll_0_iff::Fin.intrs)) 1);
-by (step_tac (!claset) 1);
+by (Clarify_tac 1);
 by (subgoal_tac "EX u. u:A" 1);
 by (etac exE 1);
 by (resolve_tac [Diff_sing_eqpoll RS revcut_rl] 1);
diff -r bed0ba7bff2f -r 39ee3d31cfbc src/ZF/Order.ML
--- a/src/ZF/Order.ML	Mon Sep 29 11:52:25 1997 +0200
+++ b/src/ZF/Order.ML	Mon Sep 29 11:56:04 1997 +0200
@@ -188,7 +188,7 @@
 
 goalw Order.thy [mono_map_def, inj_def] 
     "!!f. [| linear(A,r);  wf[B](s);  f: mono_map(A,r,B,s) |] ==> f: inj(A,B)";
-by (step_tac (!claset) 1);
+by (Clarify_tac 1);
 by (linear_case_tac 1);
 by (REPEAT 
     (EVERY [eresolve_tac [wf_on_not_refl RS notE] 1,
@@ -542,7 +542,7 @@
 by (forward_tac [well_ord_is_wf] 1);
 by (rewrite_goals_tac [wf_on_def, wf_def]);
 by (dres_inst_tac [("x", "A-domain(ord_iso_map(A,r,B,s))")] spec 1);
-by (step_tac (!claset) 1);
+by Safe_tac;
 (*The first case: the domain equals A*)
 by (rtac (domain_ord_iso_map RS equalityI) 1);
 by (etac (Diff_eq_0_iff RS iffD1) 1);
diff -r bed0ba7bff2f -r 39ee3d31cfbc src/ZF/OrderType.ML
--- a/src/ZF/OrderType.ML	Mon Sep 29 11:52:25 1997 +0200
+++ b/src/ZF/OrderType.ML	Mon Sep 29 11:56:04 1997 +0200
@@ -712,9 +712,9 @@
 \        EX j' i'. k = j**i' ++ j' & j'<j & i'<i";
 by (asm_full_simp_tac (!simpset addsimps [ordertype_pred_unfold, 
                                        well_ord_rmult, well_ord_Memrel]) 1);
-by (step_tac (!claset addSEs [ltE]) 1);
+by (safe_tac (!claset addSEs [ltE]));
 by (asm_simp_tac (!simpset addsimps [ordertype_pred_Pair_lemma, ltI,
-                                  symmetric omult_def]) 1);
+				     symmetric omult_def]) 1);
 by (blast_tac (!claset addIs [ltI]) 1);
 qed "lt_omult";
 
diff -r bed0ba7bff2f -r 39ee3d31cfbc src/ZF/Ordinal.ML
--- a/src/ZF/Ordinal.ML	Mon Sep 29 11:52:25 1997 +0200
+++ b/src/ZF/Ordinal.ML	Mon Sep 29 11:56:04 1997 +0200
@@ -403,10 +403,7 @@
 by (rtac (impI RS allI) 1);
 by (trans_ind_tac "j" [] 1);
 by (DEPTH_SOLVE (Step_tac 1 ORELSE Ord_trans_tac 1));
-qed "Ord_linear_lemma";
-
-(*"[| Ord(i); Ord(x) |] ==> i:x | i=x | x:i"*)
-bind_thm ("Ord_linear", Ord_linear_lemma RS spec RS mp);
+qed_spec_mp "Ord_linear";
 
 (*The trichotomy law for ordinals!*)
 val ordi::ordj::prems = goalw Ordinal.thy [lt_def]
diff -r bed0ba7bff2f -r 39ee3d31cfbc src/ZF/Univ.ML
--- a/src/ZF/Univ.ML	Mon Sep 29 11:52:25 1997 +0200
+++ b/src/ZF/Univ.ML	Mon Sep 29 11:56:04 1997 +0200
@@ -28,10 +28,7 @@
 by (etac (bspec RS spec RS mp) 1);
 by (assume_tac 1);
 by (rtac subset_refl 1);
-qed "Vfrom_mono_lemma";
-
-(*  [| A<=B; i<=x |] ==> Vfrom(A,i) <= Vfrom(B,x)  *)
-bind_thm ("Vfrom_mono", (Vfrom_mono_lemma RS spec RS mp));
+qed_spec_mp "Vfrom_mono";
 
 
 (** A fundamental equality: Vfrom does not require ordinals! **)
@@ -420,21 +417,18 @@
 by (rtac UN_succ_least_lt 1);
 by (Blast_tac 2);
 by (REPEAT (ares_tac [ltI] 1));
-qed "Vset_rank_imp1";
-
-(*  [| Ord(i); x : Vset(i) |] ==> rank(x) < i  *)
-bind_thm ("VsetD", (Vset_rank_imp1 RS spec RS mp));
+qed_spec_mp "VsetD";
 
 val [ordi] = goal Univ.thy "Ord(i) ==> ALL b. rank(b) : i --> b : Vset(i)";
 by (rtac (ordi RS trans_induct) 1);
 by (rtac allI 1);
 by (stac Vset 1);
 by (blast_tac (!claset addSIs [rank_lt RS ltD]) 1);
-qed "Vset_rank_imp2";
+val lemma = result();
 
 goal Univ.thy "!!x i. rank(x)<i ==> x : Vset(i)";
 by (etac ltE 1);
-by (etac (Vset_rank_imp2 RS spec RS mp) 1);
+by (etac (lemma RS spec RS mp) 1);
 by (assume_tac 1);
 qed "VsetI";