src/HOL/Nat.thy
changeset 67091 1393c2340eec
parent 67050 1e29e2666a15
child 67332 cb96edae56ef
     1.1 --- a/src/HOL/Nat.thy	Sat Nov 11 18:33:35 2017 +0000
     1.2 +++ b/src/HOL/Nat.thy	Sun Nov 26 21:08:32 2017 +0100
     1.3 @@ -360,10 +360,10 @@
     1.4    for m n :: nat
     1.5    by (cases m) simp_all
     1.6  
     1.7 -lemma add_is_1: "m + n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = 0 | m = 0 \<and> n = Suc 0"
     1.8 +lemma add_is_1: "m + n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = 0 \<or> m = 0 \<and> n = Suc 0"
     1.9    by (cases m) simp_all
    1.10  
    1.11 -lemma one_is_add: "Suc 0 = m + n \<longleftrightarrow> m = Suc 0 \<and> n = 0 | m = 0 \<and> n = Suc 0"
    1.12 +lemma one_is_add: "Suc 0 = m + n \<longleftrightarrow> m = Suc 0 \<and> n = 0 \<or> m = 0 \<and> n = Suc 0"
    1.13    by (rule trans, rule eq_commute, rule add_is_1)
    1.14  
    1.15  lemma add_eq_self_zero: "m + n = m \<Longrightarrow> n = 0"
    1.16 @@ -735,7 +735,7 @@
    1.17    for m n :: nat
    1.18    unfolding less_le ..
    1.19  
    1.20 -lemma nat_le_linear: "m \<le> n | n \<le> m"
    1.21 +lemma nat_le_linear: "m \<le> n \<or> n \<le> m"
    1.22    for m n :: nat
    1.23    by (rule linear)
    1.24