# HG changeset patch
# User wenzelm
# Date 1464010213 -7200
# Node ID fe31996e3898257268b062d34c3c54fcb11b9d97
# Parent  6813818baa6713410b3a079c8416c755b8fa4ced
removed odd cases rule (see also 8cb42cd97579);

diff -r 6813818baa67 -r fe31996e3898 NEWS
--- a/NEWS	Mon May 23 15:29:38 2016 +0200
+++ b/NEWS	Mon May 23 15:30:13 2016 +0200
@@ -117,6 +117,9 @@
     INCOMPATIBILITY.
   - The "size" plugin has been made compatible again with locales.
 
+* Removed obsolete theorem nat_less_cases. INCOMPATIBILITY, use
+linorder_cases instead.
+
 * Renamed split_if -> if_split and split_if_asm -> if_split_asm to
 resemble the f.split naming convention, INCOMPATIBILITY.
 
diff -r 6813818baa67 -r fe31996e3898 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon May 23 15:29:38 2016 +0200
+++ b/src/HOL/Nat.thy	Mon May 23 15:30:13 2016 +0200
@@ -526,19 +526,6 @@
 lemma nat_neq_iff: "m \<noteq> n \<longleftrightarrow> m < n \<or> n < m" for m n :: nat
   by (rule linorder_neq_iff)
 
-lemma nat_less_cases:
-  fixes m n :: nat
-  assumes major: "m < n \<Longrightarrow> P n m"
-    and eq: "m = n \<Longrightarrow> P n m"
-    and less: "n < m \<Longrightarrow> P n m"
-  shows "P n m"
-  apply (rule less_linear [THEN disjE])
-  apply (erule_tac [2] disjE)
-  apply (erule less)
-  apply (erule sym [THEN eq])
-  apply (erule major)
-  done
-
 
 subsubsection \<open>Inductive (?) properties\<close>
 
@@ -1240,7 +1227,7 @@
 lemma mult_eq_self_implies_10: "m = m * n \<Longrightarrow> n = 1 \<or> m = 0" for m n :: nat
   apply (drule sym)
   apply (rule disjCI)
-  apply (rule nat_less_cases, erule_tac [2] _)
+  apply (rule linorder_cases, erule_tac [2] _)
    apply (drule_tac [2] mult_less_mono2)
     apply (auto)
   done