# HG changeset patch
# User wenzelm
# Date 974313778 -3600
# Node ID 6569febd98e58712b52181209a3de31ef5ffbca8
# Parent  040de0b97b7251ffffbd1932651193ae5880cd2a
renamed integ_le_less to int_le_less;

diff -r 040de0b97b72 -r 6569febd98e5 src/HOL/Integ/Int.ML
--- a/src/HOL/Integ/Int.ML	Wed Nov 15 19:42:33 2000 +0100
+++ b/src/HOL/Integ/Int.ML	Wed Nov 15 19:42:58 2000 +0100
@@ -243,7 +243,7 @@
 
 Goal "(w <= z) = (EX n. z = w + int n)";
 by (auto_tac (claset() addSIs [not_sym RS not0_implies_Suc],
-	      simpset() addsimps [zless_iff_Suc_zadd, integ_le_less]));
+	      simpset() addsimps [zless_iff_Suc_zadd, int_le_less]));
 qed "zle_iff_zadd";
 
 
diff -r 040de0b97b72 -r 6569febd98e5 src/HOL/Integ/IntDef.ML
--- a/src/HOL/Integ/IntDef.ML	Wed Nov 15 19:42:33 2000 +0100
+++ b/src/HOL/Integ/IntDef.ML	Wed Nov 15 19:42:58 2000 +0100
@@ -451,10 +451,10 @@
 
 Goal "(x <= (y::int)) = (x < y | x=y)";
 by (REPEAT(ares_tac [iffI, zless_or_eq_imp_zle, zle_imp_zless_or_eq] 1));
-qed "integ_le_less";
+qed "int_le_less";
 
 Goal "w <= (w::int)";
-by (simp_tac (simpset() addsimps [integ_le_less]) 1);
+by (simp_tac (simpset() addsimps [int_le_less]) 1);
 qed "zle_refl";
 
 Goalw [zle_def] "z < w ==> z <= (w::int)";
@@ -463,7 +463,7 @@
 
 (* Axiom 'linorder_linear' of class 'linorder': *)
 Goal "(z::int) <= w | w <= z";
-by (simp_tac (simpset() addsimps [integ_le_less]) 1);
+by (simp_tac (simpset() addsimps [int_le_less]) 1);
 by (cut_facts_tac [zless_linear] 1);
 by (Blast_tac 1);
 qed "zle_linear";