--- a/src/HOL/UNITY/Token.ML Thu Mar 09 16:09:56 2000 +0100
+++ b/src/HOL/UNITY/Token.ML Thu Mar 09 16:14:37 2000 +0100
@@ -51,7 +51,7 @@
Goalw [nodeOrder_def, next_def, inv_image_def]
"[| i<N; j<N |] ==> ((next i, i) : nodeOrder j) = (i ~= j)";
by (auto_tac (claset(),
- simpset() addsimps [Suc_lessI, mod_Suc, mod_less, mod_geq]));
+ simpset() addsimps [Suc_lessI, mod_Suc, mod_geq]));
by (subgoal_tac "(j + N - i) = Suc (j + N - Suc i)" 1);
by (asm_simp_tac (simpset() addsimps [Suc_diff_Suc, Suc_leI, less_imp_le,
diff_add_assoc]) 2);
@@ -60,7 +60,7 @@
by (auto_tac (claset(),
simpset() addsimps [diff_add_assoc2, linorder_neq_iff,
Suc_le_eq, Suc_diff_Suc, less_imp_diff_less,
- add_diff_less, mod_less, mod_geq]));
+ add_diff_less, mod_geq]));
qed "nodeOrder_eq";
--- a/src/HOL/ex/Fib.ML Thu Mar 09 16:09:56 2000 +0100
+++ b/src/HOL/ex/Fib.ML Thu Mar 09 16:14:37 2000 +0100
@@ -62,10 +62,10 @@
by (stac fib_Suc3 3);
by (ALLGOALS (*using [fib_Suc_Suc] here results in a longer proof!*)
(asm_simp_tac (simpset() addsimps [add_mult_distrib, add_mult_distrib2,
- mod_less, mod_Suc])));
+ mod_Suc])));
by (asm_full_simp_tac
(simpset() addsimps [fib_Suc_Suc, add_mult_distrib, add_mult_distrib2,
- mod_less, mod_Suc]) 2);
+ mod_Suc]) 2);
by (ALLGOALS (asm_simp_tac (simpset() addsimps add_ac @ [fib_Suc_Suc])));
qed "fib_Cassini";
@@ -101,7 +101,7 @@
by (res_inst_tac [("n","n")] less_induct 1);
by (stac mod_if 1);
by (Asm_simp_tac 1);
-by (asm_simp_tac (simpset() addsimps [gcd_fib_diff, mod_less, mod_geq,
+by (asm_simp_tac (simpset() addsimps [gcd_fib_diff, mod_geq,
not_less_iff_le, diff_less]) 1);
qed "gcd_fib_mod";