# HG changeset patch
# User wenzelm
# Date 1205868809 -3600
# Node ID cb3badaa192eaeaba1f7e4cef4ece7159dee0a18
# Parent  9c39fc898fff67b8dd38e76ca249abc1dd9795ce
removed redundant less_trans, less_linear, le_imp_less_or_eq, le_less_trans, less_le_trans (cf. Orderings.thy);
renamed less_imp_le to less_imp_le_nat;

diff -r 9c39fc898fff -r cb3badaa192e NEWS
--- a/NEWS	Tue Mar 18 20:33:28 2008 +0100
+++ b/NEWS	Tue Mar 18 20:33:29 2008 +0100
@@ -40,6 +40,12 @@
 
 *** HOL ***
 
+* Theory Nat: renamed less_imp_le to less_imp_le_nat; removed
+redundant lemmas less_trans, less_linear, le_imp_less_or_eq,
+le_less_trans, less_le_trans, which merely duplicate lemmas of the
+same name in theory Orderings.  Potential INCOMPATIBILITY due to more
+general and different variable names.
+
 * Library/Option_ord.thy: Canonical order on option type.
 
 * Library/RBT.thy: New theory of red-black trees, an efficient
diff -r 9c39fc898fff -r cb3badaa192e src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Tue Mar 18 20:33:28 2008 +0100
+++ b/src/HOL/Nat.thy	Tue Mar 18 20:33:29 2008 +0100
@@ -386,7 +386,8 @@
 lemma Suc_lessD: "Suc m < n \<Longrightarrow> m < n"
   by (simp add: less_eq_Suc_le) (erule Suc_leD)
 
-instance proof
+instance
+proof
   fix n m :: nat
   have less_imp_le: "n < m \<Longrightarrow> n \<le> m"
     unfolding less_eq_Suc_le by (erule Suc_leD)
@@ -435,8 +436,6 @@
 lemma zero_less_Suc [iff]: "0 < Suc n"
   by (simp add: less_Suc_eq_le)
 
-lemma less_trans: "i < j ==> j < k ==> i < (k::nat)"
-  by (rule order_less_trans)
 
 subsubsection {* Elimination properties *}
 
@@ -478,9 +477,6 @@
 lemma Suc_mono: "m < n ==> Suc m < Suc n"
   by simp
 
-lemma less_linear: "m < n | m = n | n < (m::nat)"
-  by (rule less_linear)
-
 text {* "Less than" is antisymmetric, sort of *}
 lemma less_antisym: "\<lbrakk> \<not> n < m; n < Suc m \<rbrakk> \<Longrightarrow> m = n"
   unfolding not_less less_Suc_eq_le by (rule antisym)
@@ -569,18 +565,15 @@
 lemma Suc_le_lessD: "Suc m \<le> n ==> m < n"
   unfolding Suc_le_eq .
 
-lemma less_imp_le: "m < n ==> m \<le> (n::nat)"
+lemma less_imp_le_nat: "m < n ==> m \<le> (n::nat)"
   unfolding less_eq_Suc_le by (rule Suc_leD)
 
 text {* For instance, @{text "(Suc m < Suc n) = (Suc m \<le> n) = (m < n)"} *}
-lemmas le_simps = less_imp_le less_Suc_eq_le Suc_le_eq
+lemmas le_simps = less_imp_le_nat less_Suc_eq_le Suc_le_eq
 
 
 text {* Equivalence of @{term "m \<le> n"} and @{term "m < n | m = n"} *}
 
-lemma le_imp_less_or_eq: "m \<le> n ==> m < n | m = (n::nat)"
-  unfolding le_less .
-
 lemma less_or_eq_imp_le: "m < n | m = n ==> m \<le> (n::nat)"
   unfolding le_less .
 
@@ -594,12 +587,6 @@
 lemma le_refl: "n \<le> (n::nat)"
   by simp
 
-lemma le_less_trans: "[| i \<le> j; j < k |] ==> i < (k::nat)"
-  by (rule order_le_less_trans)
-
-lemma less_le_trans: "[| i < j; j \<le> k |] ==> i < (k::nat)"
-  by (rule order_less_le_trans)
-
 lemma le_trans: "[| i \<le> j; j \<le> k |] ==> i \<le> (k::nat)"
   by (rule order_trans)