--- a/arith.ML Tue Jan 04 18:33:20 1994 +0100
+++ b/arith.ML Wed Jan 05 19:37:07 1994 +0100
@@ -32,9 +32,9 @@
(*** Simplification over add, mult, diff ***)
-val arith_simps = [add_0, add_Suc,
- mult_0, mult_Suc,
- diff_0, diff_0_eq_0, diff_Suc_Suc];
+val arith_simps =
+ [pred_0, pred_Suc, add_0, add_Suc, mult_0, mult_Suc,
+ diff_0, diff_0_eq_0, diff_Suc_Suc];
val arith_ss = nat_ss addsimps arith_simps;
@@ -201,7 +201,7 @@
goal Arith.thy "P(k) --> (!n. P(Suc(n))--> P(n)) --> P(k-i)";
by (res_inst_tac [("m","k"),("n","i")] diff_induct 1);
-by (ALLGOALS (strip_tac THEN' simp_tac arith_ss THEN' fast_tac HOL_cs));
+by (ALLGOALS (strip_tac THEN' simp_tac arith_ss THEN' TRY o fast_tac HOL_cs));
val zero_induct_lemma = result();
val prems = goal Arith.thy "[| P(k); !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";