diff -r a80ad0ac0837 -r 4a327c061870 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sat Jun 22 06:25:34 2019 +0000
+++ b/src/HOL/Nat.thy	Sat Jun 22 07:18:55 2019 +0000
@@ -1773,19 +1773,32 @@
 
 end
 
+context linordered_nonzero_semiring
+begin
+
+lemma of_nat_max: "of_nat (max x y) = max (of_nat x) (of_nat y)"
+  by (auto simp: max_def ord_class.max_def)
+
+lemma of_nat_min: "of_nat (min x y) = min (of_nat x) (of_nat y)"
+  by (auto simp: min_def ord_class.min_def)
+
+end
 
 context linordered_semidom
 begin
+
 subclass linordered_nonzero_semiring ..
+
 subclass semiring_char_0 ..
+
 end
 
-
 context linordered_idom
 begin
 
-lemma abs_of_nat [simp]: "\<bar>of_nat n\<bar> = of_nat n"
-  unfolding abs_if by auto
+lemma abs_of_nat [simp]:
+  "\<bar>of_nat n\<bar> = of_nat n"
+  by (simp add: abs_if)
 
 lemma sgn_of_nat [simp]:
   "sgn (of_nat n) = of_bool (n > 0)"