# HG changeset patch
# User wenzelm
# Date 1205946925 -3600
# Node ID 961bbcc9d85b654c9c875758a937b85a09b4071c
# Parent  80ec6cf82d953caf6509dfd06f34176a59e32074
removed redundant Nat.less_not_sym, Nat.less_asym;
renamed Nat.less_irrefl to less_irrefl_nat, no longer declared elim;

diff -r 80ec6cf82d95 -r 961bbcc9d85b NEWS
--- a/NEWS	Wed Mar 19 18:15:13 2008 +0100
+++ b/NEWS	Wed Mar 19 18:15:25 2008 +0100
@@ -44,11 +44,20 @@
 
 *** 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 types and different variable names.
+* Theory Nat: removed redundant lemmas that merely duplicate lemmas of
+the same name in theory Orderings:
+
+  less_trans
+  less_linear
+  le_imp_less_or_eq
+  le_less_trans
+  less_le_trans
+  less_not_sym
+  less_asym
+
+Renamed less_imp_le to less_imp_le_nat, and less_irrefl to
+less_irrefl_nat.  Potential INCOMPATIBILITY due to more general types
+and different variable names.
 
 * Library/Option_ord.thy: Canonical order on option type.
 
diff -r 80ec6cf82d95 -r 961bbcc9d85b src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed Mar 19 18:15:13 2008 +0100
+++ b/src/HOL/Nat.thy	Wed Mar 19 18:15:25 2008 +0100
@@ -439,28 +439,17 @@
 
 subsubsection {* Elimination properties *}
 
-lemma less_not_sym: "n < m ==> ~ m < (n::nat)"
-  by (rule order_less_not_sym)
-
-lemma less_asym:
-  assumes h1: "(n::nat) < m" and h2: "~ P ==> m < n" shows P
-  apply (rule contrapos_np)
-  apply (rule less_not_sym)
-  apply (rule h1)
-  apply (erule h2)
-  done
-
 lemma less_not_refl: "~ n < (n::nat)"
   by (rule order_less_irrefl)
 
-lemma less_irrefl [elim!]: "(n::nat) < n ==> R"
-  by (rule notE, rule less_not_refl)
+lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)"
+  by (rule not_sym) (rule less_imp_neq) 
 
 lemma less_not_refl3: "(s::nat) < t ==> s \<noteq> t"
   by (rule less_imp_neq)
 
-lemma less_not_refl2: "n < m ==> m \<noteq> (n::nat)"
-  by (rule not_sym) (rule less_imp_neq) 
+lemma less_irrefl_nat: "(n::nat) < n ==> R"
+  by (rule notE, rule less_not_refl)
 
 lemma less_zeroE: "(n::nat) < 0 ==> R"
   by (rule notE) (rule not_less0)
@@ -815,7 +804,8 @@
 
 lemma not_add_less1 [iff]: "~ (i + j < (i::nat))"
 apply (rule notI)
-apply (erule add_lessD1 [THEN less_irrefl])
+apply (drule add_lessD1)
+apply (erule less_irrefl [THEN notE])
 done
 
 lemma not_add_less2 [iff]: "~ (j + i < (i::nat))"