--- 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