src/HOL/Nat.thy
changeset 63113 fe31996e3898
parent 63111 caa0c513bbca
child 63145 703edebd1d92
     1.1 --- a/src/HOL/Nat.thy	Mon May 23 15:29:38 2016 +0200
     1.2 +++ b/src/HOL/Nat.thy	Mon May 23 15:30:13 2016 +0200
     1.3 @@ -526,19 +526,6 @@
     1.4  lemma nat_neq_iff: "m \<noteq> n \<longleftrightarrow> m < n \<or> n < m" for m n :: nat
     1.5    by (rule linorder_neq_iff)
     1.6  
     1.7 -lemma nat_less_cases:
     1.8 -  fixes m n :: nat
     1.9 -  assumes major: "m < n \<Longrightarrow> P n m"
    1.10 -    and eq: "m = n \<Longrightarrow> P n m"
    1.11 -    and less: "n < m \<Longrightarrow> P n m"
    1.12 -  shows "P n m"
    1.13 -  apply (rule less_linear [THEN disjE])
    1.14 -  apply (erule_tac [2] disjE)
    1.15 -  apply (erule less)
    1.16 -  apply (erule sym [THEN eq])
    1.17 -  apply (erule major)
    1.18 -  done
    1.19 -
    1.20  
    1.21  subsubsection \<open>Inductive (?) properties\<close>
    1.22  
    1.23 @@ -1240,7 +1227,7 @@
    1.24  lemma mult_eq_self_implies_10: "m = m * n \<Longrightarrow> n = 1 \<or> m = 0" for m n :: nat
    1.25    apply (drule sym)
    1.26    apply (rule disjCI)
    1.27 -  apply (rule nat_less_cases, erule_tac [2] _)
    1.28 +  apply (rule linorder_cases, erule_tac [2] _)
    1.29     apply (drule_tac [2] mult_less_mono2)
    1.30      apply (auto)
    1.31    done