--- a/src/HOL/Integ/Int.ML Fri Aug 11 14:53:48 2000 +0200
+++ b/src/HOL/Integ/Int.ML Sat Aug 12 21:41:42 2000 +0200
@@ -104,7 +104,6 @@
simpset() addsimps [zless_iff_Suc_zadd, zadd_assoc, zadd_int]));
qed "zless_add_int_Suc_eq";
-
Goal "(w + int (Suc m) <= z) = (w + int m < z)";
by (simp_tac (simpset() addsimps [zle_def, zless_add_int_Suc_eq]) 1);
by (auto_tac (claset() addIs [zle_anti_sym] addEs [zless_asym],
@@ -112,16 +111,6 @@
qed "add_int_Suc_zle_eq";
-(* (w < int (Suc m)) = (w < int m | w = int m) *)
-bind_thm ("less_int_Suc_eq",
- simplify (simpset())
- (read_instantiate [("z", "int 0")] zless_add_int_Suc_eq));
-
-Goal "(w <= int (Suc m)) = (w <= int m | w = int (Suc m))";
-by (simp_tac (simpset() addsimps [less_int_Suc_eq, order_le_less]) 1);
-qed "le_int_Suc_eq";
-
-
(*** Monotonicity results ***)
Goal "(v+z < w+z) = (v < (w::int))";