# HG changeset patch
# User paulson
# Date 976618765 -3600
# Node ID a4529a251b6f9f025c0c229217ea17024bf540d7
# Parent  37b9897dbf3a2fd261cf04a367eba2c5f69b7188
deleting unused rules

diff -r 37b9897dbf3a -r a4529a251b6f src/HOL/Integ/IntDef.ML
--- a/src/HOL/Integ/IntDef.ML	Tue Dec 12 11:58:44 2000 +0100
+++ b/src/HOL/Integ/IntDef.ML	Tue Dec 12 11:59:25 2000 +0100
@@ -387,13 +387,6 @@
 bind_thm ("zless_irrefl", zless_not_refl RS notE);
 AddSEs [zless_irrefl];
 
-Goal "z<w ==> w ~= (z::int)";
-by (Blast_tac 1);
-qed "zless_not_refl2";
-
-(* s < t ==> s ~= t *)
-bind_thm ("zless_not_refl3", zless_not_refl2 RS not_sym);
-
 
 (*"Less than" is a linear ordering*)
 Goalw [zless_def, neg_def, zdiff_def] 
@@ -452,10 +445,6 @@
 by (simp_tac (simpset() addsimps [int_le_less]) 1);
 qed "zle_refl";
 
-Goalw [zle_def] "z < w ==> z <= (w::int)";
-by (blast_tac (claset() addEs [zless_asym]) 1);
-qed "zless_imp_zle";
-
 (* Axiom 'linorder_linear' of class 'linorder': *)
 Goal "(z::int) <= w | w <= z";
 by (simp_tac (simpset() addsimps [int_le_less]) 1);
@@ -463,16 +452,7 @@
 by (Blast_tac 1);
 qed "zle_linear";
 
-Goal "[| i <= j; j < k |] ==> i < (k::int)";
-by (dtac zle_imp_zless_or_eq 1);
-by (blast_tac (claset() addIs [zless_trans]) 1);
-qed "zle_zless_trans";
-
-Goal "[| i < j; j <= k |] ==> i < (k::int)";
-by (dtac zle_imp_zless_or_eq 1);
-by (blast_tac (claset() addIs [zless_trans]) 1);
-qed "zless_zle_trans";
-
+(* Axiom 'order_trans of class 'order': *)
 Goal "[| i <= j; j <= k |] ==> i <= (k::int)";
 by (EVERY1 [dtac zle_imp_zless_or_eq, dtac zle_imp_zless_or_eq,
             rtac zless_or_eq_imp_zle, 
@@ -490,10 +470,6 @@
 by (blast_tac (claset() addSEs [zless_asym]) 1);
 qed "int_less_le";
 
-(* [| w <= z; w ~= z |] ==> w < z *)
-bind_thm ("zle_neq_implies_zless", [int_less_le, conjI] MRS iffD2);
-
-
 
 (*** Subtraction laws ***)