# HG changeset patch
# User paulson
# Date 966109302 -7200
# Node ID 38e58ed53e7ba33a0d135b5109daa043aa2139d9
# Parent  b295382e1549dbb65266d7801ef75a53dd4b0823
deleted needless rules

diff -r b295382e1549 -r 38e58ed53e7b src/HOL/Integ/Int.ML
--- 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))";