src/HOL/ex/Fib.ML
changeset 4385 f6d019eefa1e
parent 4379 7049ca8f912e
child 4686 74a12e86b20b
--- a/src/HOL/ex/Fib.ML	Mon Dec 08 20:29:49 1997 +0100
+++ b/src/HOL/ex/Fib.ML	Thu Dec 11 10:28:04 1997 +0100
@@ -25,7 +25,7 @@
 by (res_inst_tac [("u","n")] fib.induct 1);
 (*Simplify the LHS just enough to apply the induction hypotheses*)
 by (asm_full_simp_tac
-    (simpset() addsimps [read_instantiate[("x", "Suc(?m+?n)")] fib_Suc_Suc]) 3);
+    (simpset() addsimps [read_instantiate[("x","Suc(?m+?n)")] fib_Suc_Suc]) 3);
 by (ALLGOALS 
     (asm_simp_tac (simpset() addsimps 
 		   (fib.rules @ add_ac @ mult_ac @
@@ -58,9 +58,8 @@
 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])));
-by (safe_tac (claset() addSDs [mod2_neq_0]));
+				       mod_less, mod_Suc]
+                             addsplits [expand_if])));
 by (ALLGOALS
     (asm_full_simp_tac
      (simpset() addsimps (fib.rules @ add_ac @ mult_ac @