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