# HG changeset patch
# User nipkow
# Date 1590091575 -7200
# Node ID 76784f47c60f6562e91c19adb1a502738ea264b9
# Parent  34ecb540a07970c700ddf6344a4dc47e6bac9d46
unused alias

diff -r 34ecb540a079 -r 76784f47c60f src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Wed May 20 19:43:39 2020 +0000
+++ b/src/HOL/Nat.thy	Thu May 21 22:06:15 2020 +0200
@@ -906,9 +906,6 @@
 lemma max_Suc2: "max m (Suc n) = (case m of 0 \<Rightarrow> Suc n | Suc m' \<Rightarrow> Suc (max m' n))"
   by (simp split: nat.split)
 
-lemma max_0_iff: "max m n = (0::nat) \<longleftrightarrow> m = 0 \<and> n = 0"
-  by (fact max_nat.eq_neutr_iff)
-
 lemma nat_mult_min_left: "min m n * q = min (m * q) (n * q)"
   for m n q :: nat
   by (simp add: min_def not_le)