src/HOL/ex/Fib.ML
changeset 4686 74a12e86b20b
parent 4385 f6d019eefa1e
child 4710 05e57f1879ee
--- a/src/HOL/ex/Fib.ML	Fri Mar 06 18:25:28 1998 +0100
+++ b/src/HOL/ex/Fib.ML	Sat Mar 07 16:29:29 1998 +0100
@@ -58,8 +58,7 @@
 by (stac (read_instantiate [("x", "Suc ?n")] fib_Suc_Suc) 3);
 by (ALLGOALS  (*using fib.rules here results in a longer proof!*)
     (asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2, 
-				       mod_less, mod_Suc]
-                             addsplits [expand_if])));
+				       mod_less, mod_Suc])));
 by (ALLGOALS
     (asm_full_simp_tac
      (simpset() addsimps (fib.rules @ add_ac @ mult_ac @