# HG changeset patch
# User paulson
# Date 927276427 -7200
# Node ID 32892a8ecb1524ae0867e99626ae9c59917f3995
# Parent  ca95af28fb33169c1c97e72fb6cbfca3101bd942
deleted some vestigal theorems (use the equivalents on HOL/Ord.ML)

diff -r ca95af28fb33 -r 32892a8ecb15 src/HOL/Integ/IntDef.ML
--- a/src/HOL/Integ/IntDef.ML	Wed May 19 11:22:02 1999 +0200
+++ b/src/HOL/Integ/IntDef.ML	Fri May 21 10:47:07 1999 +0200
@@ -496,25 +496,6 @@
 qed "zle_int";
 Addsimps [zle_int];
 
-Goalw [zle_def] "~(w<z) ==> z<=(w::int)";
-by (assume_tac 1);
-qed "zleI";
-
-Goalw [zle_def] "z<=w ==> ~(w<(z::int))";
-by (assume_tac 1);
-qed "zleD";
-
-(*  [| z <= w;  ~ P ==> w < z |] ==> P  *)
-bind_thm ("zleE", zleD RS swap);
-
-Goalw [zle_def] "(~w<=z) = (z<(w::int))";
-by (Simp_tac 1);
-qed "not_zle_iff_zless";
-
-Goalw [zle_def] "~ z <= w ==> w<(z::int)";
-by (Fast_tac 1);
-qed "not_zleE";
-
 Goalw [zle_def] "z <= w ==> z < w | z=(w::int)";
 by (cut_facts_tac [zless_linear] 1);
 by (blast_tac (claset() addEs [zless_asym]) 1);