changeset 3724 | f33e301a89f5 |
parent 3300 | 4f5ffefa7799 |
child 3919 | c036caebfc75 |
--- a/src/HOL/ex/Fib.ML Mon Sep 29 11:36:44 1997 +0200 +++ b/src/HOL/ex/Fib.ML Mon Sep 29 11:37:02 1997 +0200 @@ -54,7 +54,7 @@ (asm_simp_tac (!simpset addsimps [add_mult_distrib, add_mult_distrib2, mod_less, mod_Suc] setloop split_tac[expand_if]))); -by (step_tac (!claset addSDs [mod2_neq_0]) 1); +by (safe_tac (!claset addSDs [mod2_neq_0])); by (ALLGOALS (asm_full_simp_tac (!simpset addsimps (fib.rules @ add_ac @ mult_ac @