src/HOL/Arith.ML
changeset 3718 d78cf498a88c
parent 3484 1e93eb09ebb9
child 3724 f33e301a89f5
     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)";