unused alias
authornipkow
Thu May 21 22:06:15 2020 +0200 (10 days ago)
changeset 7185276784f47c60f
parent 71851 34ecb540a079
child 71853 30d92e668b52
unused alias
src/HOL/Nat.thy
     1.1 --- a/src/HOL/Nat.thy	Wed May 20 19:43:39 2020 +0000
     1.2 +++ b/src/HOL/Nat.thy	Thu May 21 22:06:15 2020 +0200
     1.3 @@ -906,9 +906,6 @@
     1.4  lemma max_Suc2: "max m (Suc n) = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max m' n))"
     1.5    by (simp split: nat.split)
     1.6  
     1.7 -lemma max_0_iff: "max m n = (0::nat) \<longleftrightarrow> m = 0 \<and> n = 0"
     1.8 -  by (fact max_nat.eq_neutr_iff)
     1.9 -
    1.10  lemma nat_mult_min_left: "min m n * q = min (m * q) (n * q)"
    1.11    for m n q :: nat
    1.12    by (simp add: min_def not_le)