Minor tidying to use Clarify_tac, etc.
authorpaulson
Fri Sep 26 10:21:14 1997 +0200 (1997-09-26)
changeset 3718d78cf498a88c
parent 3717 e28553315355
child 3719 6a142dab2a08
Minor tidying to use Clarify_tac, etc.
src/HOL/Arith.ML
src/HOL/Divides.ML
src/HOL/Induct/Exp.ML
src/HOL/Induct/LFilter.ML
src/HOL/Induct/Mutil.ML
src/HOL/Integ/Equiv.ML
src/HOL/NatDef.ML
src/HOL/Relation.ML
src/HOL/Set.ML
src/HOL/WF_Rel.ML
src/HOL/ex/Primes.ML
     1.1 --- a/src/HOL/Arith.ML	Fri Sep 26 10:12:04 1997 +0200
     1.2 +++ b/src/HOL/Arith.ML	Fri Sep 26 10:21:14 1997 +0200
     1.3 @@ -432,7 +432,7 @@
     1.4  
     1.5  goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
     1.6  by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
     1.7 -by (ALLGOALS (strip_tac THEN' Simp_tac THEN' TRY o Blast_tac));
     1.8 +by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));
     1.9  qed "zero_induct_lemma";
    1.10  
    1.11  val prems = goal Arith.thy "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
     2.1 --- a/src/HOL/Divides.ML	Fri Sep 26 10:12:04 1997 +0200
     2.2 +++ b/src/HOL/Divides.ML	Fri Sep 26 10:21:14 1997 +0200
     2.3 @@ -121,7 +121,7 @@
     2.4  (* Monotonicity of div in first argument *)
     2.5  goal thy "!!n. 0<k ==> ALL m. m <= n --> (m div k) <= (n div k)";
     2.6  by (res_inst_tac [("n","n")] less_induct 1);
     2.7 -by (strip_tac 1);
     2.8 +by (Clarify_tac 1);
     2.9  by (case_tac "na<k" 1);
    2.10  (* 1  case n<k *)
    2.11  by (subgoal_tac "m<k" 1);
    2.12 @@ -347,7 +347,7 @@
    2.13  AddIffs [dvd_refl RS dvd_mult, dvd_refl RS dvd_mult2];
    2.14  
    2.15  goalw thy [dvd_def] "!!m. [| f dvd m; f dvd n; 0<n |] ==> f dvd (m mod n)";
    2.16 -by (Step_tac 1);
    2.17 +by (Clarify_tac 1);
    2.18  by (full_simp_tac (!simpset addsimps [zero_less_mult_iff]) 1);
    2.19  by (res_inst_tac 
    2.20      [("x", "(((k div ka)*ka + k mod ka) - ((f*k) div (f*ka)) * ka)")] 
    2.21 @@ -369,7 +369,7 @@
    2.22  qed "dvd_mult_cancel";
    2.23  
    2.24  goalw thy [dvd_def] "!!i j. [| i dvd m; j dvd n|] ==> (i*j) dvd (m*n)";
    2.25 -by (Step_tac 1);
    2.26 +by (Clarify_tac 1);
    2.27  by (res_inst_tac [("x","k*ka")] exI 1);
    2.28  by (asm_simp_tac (!simpset addsimps mult_ac) 1);
    2.29  qed "mult_dvd_mono";
    2.30 @@ -380,7 +380,7 @@
    2.31  qed "dvd_mult_left";
    2.32  
    2.33  goalw thy [dvd_def] "!!n. [| k dvd n; 0 < n |] ==> k <= n";
    2.34 -by (Step_tac 1);
    2.35 +by (Clarify_tac 1);
    2.36  by (ALLGOALS (full_simp_tac (!simpset addsimps [zero_less_mult_iff])));
    2.37  by (etac conjE 1);
    2.38  by (rtac le_trans 1);
     3.1 --- a/src/HOL/Induct/Exp.ML	Fri Sep 26 10:12:04 1997 +0200
     3.2 +++ b/src/HOL/Induct/Exp.ML	Fri Sep 26 10:21:14 1997 +0200
     3.3 @@ -80,7 +80,7 @@
     3.4  by (Blast_tac 1);
     3.5  by (blast_tac (!claset addEs [exec_WHILE_case]) 1);
     3.6  by (thin_tac "(?c,s2) -[?ev]-> s3" 1);
     3.7 -by (Step_tac 1);
     3.8 +by (Clarify_tac 1);
     3.9  by (etac exec_WHILE_case 1);
    3.10  by (ALLGOALS Fast_tac);         (*Blast_tac: proof fails*)
    3.11  qed "com_Unique";
    3.12 @@ -197,10 +197,8 @@
    3.13  qed "valof_valof";
    3.14  
    3.15  
    3.16 -
    3.17  (** Equivalence of  VALOF SKIP RESULTIS e  and  e **)
    3.18  
    3.19 -
    3.20  goal thy "!!x. (e',s) -|-> (v,s') ==> \
    3.21  \              (e' = VALOF SKIP RESULTIS e) --> \
    3.22  \              (e, s) -|-> (v,s')";
    3.23 @@ -218,7 +216,6 @@
    3.24  qed "valof_skip";
    3.25  
    3.26  
    3.27 -
    3.28  (** Equivalence of  VALOF x:=e RESULTIS x  and  e **)
    3.29  
    3.30  goal thy "!!x. (e',s) -|-> (v,s'') ==> \
    3.31 @@ -227,7 +224,7 @@
    3.32  by (etac eval_induct 1);
    3.33  by (ALLGOALS Asm_simp_tac);
    3.34  by (thin_tac "?PP-->?QQ" 1);
    3.35 -by (Step_tac 1);
    3.36 +by (Clarify_tac 1);
    3.37  by (Simp_tac 1);
    3.38  by (Blast_tac 1); 
    3.39  bind_thm ("valof_assign1", refl RSN (2, result() RS mp));
     4.1 --- a/src/HOL/Induct/LFilter.ML	Fri Sep 26 10:12:04 1997 +0200
     4.2 +++ b/src/HOL/Induct/LFilter.ML	Fri Sep 26 10:21:14 1997 +0200
     4.3 @@ -59,7 +59,7 @@
     4.4  
     4.5  val prems = goal thy
     4.6      "[| !!x. p x ==> q x |] ==> Domain (findRel p) <= Domain (findRel q)";
     4.7 -by (Step_tac 1);
     4.8 +by (Clarify_tac 1);
     4.9  by (etac findRel.induct 1);
    4.10  by (blast_tac (!claset addIs (findRel.intrs@prems)) 1);
    4.11  by (blast_tac (!claset addIs findRel.intrs) 1);
    4.12 @@ -89,7 +89,7 @@
    4.13  goal thy "!!p. ~ (p x) ==> find p (LCons x l) = find p l";
    4.14  by (case_tac "LCons x l : Domain(findRel p)" 1);
    4.15  by (Asm_full_simp_tac 2);
    4.16 -by (Step_tac 1);
    4.17 +by (Clarify_tac 1);
    4.18  by (asm_simp_tac (!simpset addsimps [findRel_imp_find]) 1);
    4.19  by (blast_tac (!claset addIs (findRel_imp_find::findRel.intrs)) 1);
    4.20  qed "find_LCons_seek";
    4.21 @@ -335,7 +335,7 @@
    4.22  by (asm_simp_tac (!simpset addsimps [diverge_lfilter_LNil]) 2);
    4.23  by (etac Domain_findRelE 1);
    4.24  by (forward_tac [lmap_LCons_findRel] 1);
    4.25 -by (Step_tac 1);
    4.26 +by (Clarify_tac 1);
    4.27  by (asm_simp_tac (!simpset addsimps [findRel_imp_lfilter]) 1);
    4.28  by (Blast_tac 1);
    4.29  qed "lfilter_lmap";
     5.1 --- a/src/HOL/Induct/Mutil.ML	Fri Sep 26 10:12:04 1997 +0200
     5.2 +++ b/src/HOL/Induct/Mutil.ML	Fri Sep 26 10:21:14 1997 +0200
     5.3 @@ -94,7 +94,8 @@
     5.4  goalw thy [evnodd_def]
     5.5      "evnodd (insert (i,j) C) b = \
     5.6  \      (if (i+j) mod 2 = b then insert (i,j) (evnodd C b) else evnodd C b)";
     5.7 -by (simp_tac (!simpset setloop (split_tac [expand_if] THEN' Step_tac)) 1);
     5.8 +by (simp_tac (!simpset setloop split_tac [expand_if]) 1);
     5.9 +by (Blast_tac 1);
    5.10  qed "evnodd_insert";
    5.11  
    5.12  Addsimps [finite_evnodd, evnodd_Un, evnodd_Diff, evnodd_empty, evnodd_insert];
    5.13 @@ -133,7 +134,7 @@
    5.14  by (Simp_tac 2 THEN assume_tac 1);
    5.15  by (res_inst_tac [("b1","1")] (domino_singleton RS exE) 1);
    5.16  by (Simp_tac 2 THEN assume_tac 1);
    5.17 -by (Step_tac 1);
    5.18 +by (Clarify_tac 1);
    5.19  by (subgoal_tac "ALL p b. p : evnodd a b --> p ~: evnodd ta b" 1);
    5.20  by (asm_simp_tac (!simpset addsimps [tiling_domino_finite]) 1);
    5.21  by (blast_tac (!claset addSDs [evnodd_subset RS subsetD] addEs [equalityE]) 1);
     6.1 --- a/src/HOL/Integ/Equiv.ML	Fri Sep 26 10:12:04 1997 +0200
     6.2 +++ b/src/HOL/Integ/Equiv.ML	Fri Sep 26 10:21:14 1997 +0200
     6.3 @@ -18,19 +18,19 @@
     6.4  
     6.5  goalw Equiv.thy [trans_def,sym_def,inverse_def]
     6.6      "!!r. [| sym(r); trans(r) |] ==> r^-1 O r <= r";
     6.7 -by (fast_tac (!claset addSEs [inverseD]) 1);
     6.8 +by (blast_tac (!claset addSEs [inverseD]) 1);
     6.9  qed "sym_trans_comp_subset";
    6.10  
    6.11  goalw Equiv.thy [refl_def]
    6.12      "!!A r. refl A r ==> r <= r^-1 O r";
    6.13 -by (fast_tac (!claset addIs [compI]) 1);
    6.14 +by (Blast_tac 1);
    6.15  qed "refl_comp_subset";
    6.16  
    6.17  goalw Equiv.thy [equiv_def]
    6.18      "!!A r. equiv A r ==> r^-1 O r = r";
    6.19 +by (Clarify_tac 1);
    6.20  by (rtac equalityI 1);
    6.21 -by (REPEAT (ares_tac [sym_trans_comp_subset, refl_comp_subset] 1
    6.22 -     ORELSE etac conjE 1));
    6.23 +by (REPEAT (ares_tac [sym_trans_comp_subset, refl_comp_subset] 1));
    6.24  qed "equiv_comp_eq";
    6.25  
    6.26  (*second half*)
    6.27 @@ -38,9 +38,7 @@
    6.28      "!!A r. [| r^-1 O r = r;  Domain(r) = A |] ==> equiv A r";
    6.29  by (etac equalityE 1);
    6.30  by (subgoal_tac "ALL x y. (x,y) : r --> (y,x) : r" 1);
    6.31 -by (Step_tac 1);
    6.32 -by (fast_tac (!claset addIs [compI]) 3);
    6.33 -by (ALLGOALS (fast_tac (!claset addIs [compI])));
    6.34 +by (ALLGOALS Fast_tac);
    6.35  qed "comp_equivI";
    6.36  
    6.37  (** Equivalence classes **)
    6.38 @@ -48,27 +46,24 @@
    6.39  (*Lemma for the next result*)
    6.40  goalw Equiv.thy [equiv_def,trans_def,sym_def]
    6.41      "!!A r. [| equiv A r;  (a,b): r |] ==> r^^{a} <= r^^{b}";
    6.42 -by (Step_tac 1);
    6.43 -by (rtac ImageI 1);
    6.44 -by (Fast_tac 2);
    6.45 -by (Fast_tac 1);
    6.46 +by (Blast_tac 1);
    6.47  qed "equiv_class_subset";
    6.48  
    6.49  goal Equiv.thy "!!A r. [| equiv A r;  (a,b): r |] ==> r^^{a} = r^^{b}";
    6.50  by (REPEAT (ares_tac [equalityI, equiv_class_subset] 1));
    6.51  by (rewrite_goals_tac [equiv_def,sym_def]);
    6.52 -by (Fast_tac 1);
    6.53 +by (Blast_tac 1);
    6.54  qed "equiv_class_eq";
    6.55  
    6.56  goalw Equiv.thy [equiv_def,refl_def]
    6.57      "!!A r. [| equiv A r;  a: A |] ==> a: r^^{a}";
    6.58 -by (Fast_tac 1);
    6.59 +by (Blast_tac 1);
    6.60  qed "equiv_class_self";
    6.61  
    6.62  (*Lemma for the next result*)
    6.63  goalw Equiv.thy [equiv_def,refl_def]
    6.64      "!!A r. [| equiv A r;  r^^{b} <= r^^{a};  b: A |] ==> (a,b): r";
    6.65 -by (Fast_tac 1);
    6.66 +by (Blast_tac 1);
    6.67  qed "subset_equiv_class";
    6.68  
    6.69  goal Equiv.thy
    6.70 @@ -79,7 +74,7 @@
    6.71  (*thus r^^{a} = r^^{b} as well*)
    6.72  goalw Equiv.thy [equiv_def,trans_def,sym_def]
    6.73      "!!A r. [| equiv A r;  x: (r^^{a} Int r^^{b}) |] ==> (a,b): r";
    6.74 -by (Fast_tac 1);
    6.75 +by (Blast_tac 1);
    6.76  qed "equiv_class_nondisjoint";
    6.77  
    6.78  val [major] = goalw Equiv.thy [equiv_def,refl_def]
    6.79 @@ -89,23 +84,14 @@
    6.80  
    6.81  goal Equiv.thy
    6.82      "!!A r. equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
    6.83 -by (Step_tac 1);
    6.84 -by ((rtac equiv_class_eq 1) THEN (assume_tac 1) THEN (assume_tac 1));
    6.85 -by ((rtac eq_equiv_class 3) THEN 
    6.86 -    (assume_tac 4) THEN (assume_tac 4) THEN (assume_tac 3));
    6.87 -by ((dtac equiv_type 1) THEN (dtac rev_subsetD 1) THEN
    6.88 -    (assume_tac 1) THEN (dtac SigmaD1 1) THEN (assume_tac 1));
    6.89 -by ((dtac equiv_type 1) THEN (dtac rev_subsetD 1) THEN
    6.90 -    (assume_tac 1) THEN (dtac SigmaD2 1) THEN (assume_tac 1));
    6.91 +by (blast_tac (!claset addSIs [equiv_class_eq]
    6.92 +	               addDs [eq_equiv_class, equiv_type]) 1);
    6.93  qed "equiv_class_eq_iff";
    6.94  
    6.95  goal Equiv.thy
    6.96      "!!A r. [| equiv A r;  x: A;  y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
    6.97 -by (Step_tac 1);
    6.98 -by ((rtac eq_equiv_class 1) THEN 
    6.99 -    (assume_tac 1) THEN (assume_tac 1) THEN (assume_tac 1));
   6.100 -by ((rtac equiv_class_eq 1) THEN 
   6.101 -    (assume_tac 1) THEN (assume_tac 1));
   6.102 +by (blast_tac (!claset addSIs [equiv_class_eq]
   6.103 +	               addDs [eq_equiv_class, equiv_type]) 1);
   6.104  qed "eq_equiv_class_iff";
   6.105  
   6.106  (*** Quotients ***)
   6.107 @@ -113,7 +99,7 @@
   6.108  (** Introduction/elimination rules -- needed? **)
   6.109  
   6.110  goalw Equiv.thy [quotient_def] "!!A. x:A ==> r^^{x}: A/r";
   6.111 -by (Fast_tac 1);
   6.112 +by (Blast_tac 1);
   6.113  qed "quotientI";
   6.114  
   6.115  val [major,minor] = goalw Equiv.thy [quotient_def]
   6.116 @@ -122,7 +108,7 @@
   6.117  by (resolve_tac [major RS UN_E] 1);
   6.118  by (rtac minor 1);
   6.119  by (assume_tac 2);
   6.120 -by (Fast_tac 1);
   6.121 +by (Fast_tac 1);   (*Blast_tac FAILS to prove it*)
   6.122  qed "quotientE";
   6.123  
   6.124  goalw Equiv.thy [equiv_def,refl_def,quotient_def]
   6.125 @@ -157,7 +143,7 @@
   6.126  \                      ==> (UN x:r^^{a}. b(x)) = b(a)";
   6.127  by (rtac (equiv_class_self RS UN_singleton) 1 THEN REPEAT (assume_tac 1));
   6.128  by (rewrite_goals_tac [equiv_def,congruent_def,sym_def]);
   6.129 -by (Fast_tac 1);
   6.130 +by (Blast_tac 1);
   6.131  qed "UN_equiv_class";
   6.132  
   6.133  (*type checking of  UN x:r``{a}. b(x) *)
   6.134 @@ -166,7 +152,7 @@
   6.135  \       !!x.  x : A ==> b(x) : B |]             \
   6.136  \    ==> (UN x:X. b(x)) : B";
   6.137  by (cut_facts_tac prems 1);
   6.138 -by (Step_tac 1);
   6.139 +by (Clarify_tac 1);
   6.140  by (stac UN_equiv_class 1);
   6.141  by (REPEAT (ares_tac prems 1));
   6.142  qed "UN_equiv_class_type";
   6.143 @@ -180,7 +166,7 @@
   6.144  \       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> (x,y):r |]         \
   6.145  \    ==> X=Y";
   6.146  by (cut_facts_tac prems 1);
   6.147 -by (Step_tac 1);
   6.148 +by (Clarify_tac 1);
   6.149  by (rtac equiv_class_eq 1);
   6.150  by (REPEAT (ares_tac prems 1));
   6.151  by (etac box_equals 1);
   6.152 @@ -193,18 +179,18 @@
   6.153  
   6.154  goalw Equiv.thy [congruent_def,congruent2_def,equiv_def,refl_def]
   6.155      "!!A r. [| equiv A r;  congruent2 r b;  a: A |] ==> congruent r (b a)";
   6.156 -by (Fast_tac 1);
   6.157 +by (Blast_tac 1);
   6.158  qed "congruent2_implies_congruent";
   6.159  
   6.160  goalw Equiv.thy [congruent_def]
   6.161      "!!A r. [| equiv A r;  congruent2 r b;  a: A |] ==> \
   6.162  \    congruent r (%x1. UN x2:r^^{a}. b x1 x2)";
   6.163 -by (Step_tac 1);
   6.164 +by (Clarify_tac 1);
   6.165  by (rtac (equiv_type RS subsetD RS SigmaE2) 1 THEN REPEAT (assume_tac 1));
   6.166  by (asm_simp_tac (!simpset addsimps [UN_equiv_class,
   6.167                                       congruent2_implies_congruent]) 1);
   6.168  by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
   6.169 -by (Fast_tac 1);
   6.170 +by (Blast_tac 1);
   6.171  qed "congruent2_implies_congruent_UN";
   6.172  
   6.173  goal Equiv.thy
   6.174 @@ -222,7 +208,7 @@
   6.175  \       !!x1 x2.  [| x1: A; x2: A |] ==> b x1 x2 : B |]    \
   6.176  \    ==> (UN x1:X1. UN x2:X2. b x1 x2) : B";
   6.177  by (cut_facts_tac prems 1);
   6.178 -by (Step_tac 1);
   6.179 +by (Clarify_tac 1);
   6.180  by (REPEAT (ares_tac (prems@[UN_equiv_class_type,
   6.181                               congruent2_implies_congruent_UN,
   6.182                               congruent2_implies_congruent, quotientI]) 1));
   6.183 @@ -237,10 +223,8 @@
   6.184  \       !! y z w. [| w: A;  (y,z) : r |] ==> b w y = b w z       \
   6.185  \    |] ==> congruent2 r b";
   6.186  by (cut_facts_tac prems 1);
   6.187 -by (Step_tac 1);
   6.188 -by (rtac trans 1);
   6.189 -by (REPEAT (ares_tac prems 1
   6.190 -     ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1));
   6.191 +by (Clarify_tac 1);
   6.192 +by (blast_tac (!claset addIs (trans::prems)) 1);
   6.193  qed "congruent2I";
   6.194  
   6.195  val [equivA,commute,congt] = goal Equiv.thy
     7.1 --- a/src/HOL/NatDef.ML	Fri Sep 26 10:12:04 1997 +0200
     7.2 +++ b/src/HOL/NatDef.ML	Fri Sep 26 10:21:14 1997 +0200
     7.3 @@ -152,7 +152,7 @@
     7.4  qed "nat_case_Suc";
     7.5  
     7.6  goalw thy [wf_def, pred_nat_def] "wf(pred_nat)";
     7.7 -by (strip_tac 1);
     7.8 +by (Clarify_tac 1);
     7.9  by (nat_ind_tac "x" 1);
    7.10  by (ALLGOALS Blast_tac);
    7.11  qed "wf_pred_nat";
     8.1 --- a/src/HOL/Relation.ML	Fri Sep 26 10:12:04 1997 +0200
     8.2 +++ b/src/HOL/Relation.ML	Fri Sep 26 10:21:14 1997 +0200
     8.3 @@ -164,7 +164,7 @@
     8.4      "[| b: r^^A;  !!x.[| (x,b): r;  x:A |] ==> P |] ==> P"
     8.5   (fn major::prems=>
     8.6    [ (rtac (major RS CollectE) 1),
     8.7 -    (Step_tac 1),
     8.8 +    (Clarify_tac 1),
     8.9      (rtac (hd prems) 1),
    8.10      (REPEAT (etac bexE 1 ORELSE ares_tac prems 1)) ]);
    8.11  
     9.1 --- a/src/HOL/Set.ML	Fri Sep 26 10:12:04 1997 +0200
     9.2 +++ b/src/HOL/Set.ML	Fri Sep 26 10:21:14 1997 +0200
     9.3 @@ -412,8 +412,8 @@
     9.4  
     9.5  (*Redundant? But unlike insertCI, it proves the subgoal immediately!*)
     9.6  AddSIs [singletonI];   
     9.7 -    
     9.8  AddSDs [singleton_inject];
     9.9 +AddSEs [singletonE];
    9.10  
    9.11  goal Set.thy "{x.x=a} = {a}";
    9.12  by(Blast_tac 1);
    10.1 --- a/src/HOL/WF_Rel.ML	Fri Sep 26 10:12:04 1997 +0200
    10.2 +++ b/src/HOL/WF_Rel.ML	Fri Sep 26 10:21:14 1997 +0200
    10.3 @@ -34,7 +34,7 @@
    10.4  
    10.5  goal thy "!!r. wf(r) ==> wf(inv_image r (f::'a=>'b))"; 
    10.6  by (full_simp_tac (!simpset addsimps [inv_image_def, wf_eq_minimal]) 1);
    10.7 -by (Step_tac 1);
    10.8 +by (Clarify_tac 1);
    10.9  by (subgoal_tac "? (w::'b). w : {w. ? (x::'a). x: Q & (f x = w)}" 1);
   10.10  by (blast_tac (!claset delrules [allE]) 2);
   10.11  by (etac allE 1);
   10.12 @@ -130,7 +130,7 @@
   10.13   by (Blast_tac 1);
   10.14  by (etac swap 1);
   10.15  by (Asm_full_simp_tac 1);
   10.16 -by (Step_tac 1);
   10.17 +by (Clarify_tac 1);
   10.18  by (subgoal_tac "!n. nat_rec x (%i y. @z. z:Q & (z,y):r) n : Q" 1);
   10.19   by (res_inst_tac[("x","nat_rec x (%i y. @z. z:Q & (z,y):r)")]exI 1);
   10.20   by (rtac allI 1);
    11.1 --- a/src/HOL/ex/Primes.ML	Fri Sep 26 10:12:04 1997 +0200
    11.2 +++ b/src/HOL/ex/Primes.ML	Fri Sep 26 10:21:14 1997 +0200
    11.3 @@ -90,7 +90,7 @@
    11.4  (*This theorem leads immediately to a proof of the uniqueness of factorization.
    11.5    If p divides a product of primes then it is one of those primes.*)
    11.6  goalw thy [prime_def] "!!p. [| p: prime; p dvd (m*n) |] ==> p dvd m | p dvd n";
    11.7 -by (Step_tac 1);
    11.8 +by (Clarify_tac 1);
    11.9  by (subgoal_tac "m = gcd(m*p, m*n)" 1);
   11.10  by (etac ssubst 1);
   11.11  by (rtac gcd_greatest 1);