removed odd cases rule (see also 8cb42cd97579);
authorwenzelm
Mon May 23 15:30:13 2016 +0200 (2016-05-23)
changeset 63113fe31996e3898
parent 63112 6813818baa67
child 63115 39dca4891601
child 63117 acb6d72fc42e
removed odd cases rule (see also 8cb42cd97579);
NEWS
src/HOL/Nat.thy
     1.1 --- a/NEWS	Mon May 23 15:29:38 2016 +0200
     1.2 +++ b/NEWS	Mon May 23 15:30:13 2016 +0200
     1.3 @@ -117,6 +117,9 @@
     1.4      INCOMPATIBILITY.
     1.5    - The "size" plugin has been made compatible again with locales.
     1.6  
     1.7 +* Removed obsolete theorem nat_less_cases. INCOMPATIBILITY, use
     1.8 +linorder_cases instead.
     1.9 +
    1.10  * Renamed split_if -> if_split and split_if_asm -> if_split_asm to
    1.11  resemble the f.split naming convention, INCOMPATIBILITY.
    1.12  
     2.1 --- a/src/HOL/Nat.thy	Mon May 23 15:29:38 2016 +0200
     2.2 +++ b/src/HOL/Nat.thy	Mon May 23 15:30:13 2016 +0200
     2.3 @@ -526,19 +526,6 @@
     2.4  lemma nat_neq_iff: "m \<noteq> n \<longleftrightarrow> m < n \<or> n < m" for m n :: nat
     2.5    by (rule linorder_neq_iff)
     2.6  
     2.7 -lemma nat_less_cases:
     2.8 -  fixes m n :: nat
     2.9 -  assumes major: "m < n \<Longrightarrow> P n m"
    2.10 -    and eq: "m = n \<Longrightarrow> P n m"
    2.11 -    and less: "n < m \<Longrightarrow> P n m"
    2.12 -  shows "P n m"
    2.13 -  apply (rule less_linear [THEN disjE])
    2.14 -  apply (erule_tac [2] disjE)
    2.15 -  apply (erule less)
    2.16 -  apply (erule sym [THEN eq])
    2.17 -  apply (erule major)
    2.18 -  done
    2.19 -
    2.20  
    2.21  subsubsection \<open>Inductive (?) properties\<close>
    2.22  
    2.23 @@ -1240,7 +1227,7 @@
    2.24  lemma mult_eq_self_implies_10: "m = m * n \<Longrightarrow> n = 1 \<or> m = 0" for m n :: nat
    2.25    apply (drule sym)
    2.26    apply (rule disjCI)
    2.27 -  apply (rule nat_less_cases, erule_tac [2] _)
    2.28 +  apply (rule linorder_cases, erule_tac [2] _)
    2.29     apply (drule_tac [2] mult_less_mono2)
    2.30      apply (auto)
    2.31    done