--- a/src/HOL/Nat.thy Fri Feb 12 16:09:07 2016 +0100
+++ b/src/HOL/Nat.thy Fri Feb 19 13:40:50 2016 +0100
@@ -752,6 +752,10 @@
instance nat :: dioid
proof qed (rule nat_le_iff_add)
+declare le0[simp del] -- \<open>This is now @{thm zero_le}\<close>
+declare le_0_eq[simp del] -- \<open>This is now @{thm le_zero_eq}\<close>
+declare not_less0[simp del] -- \<open>This is now @{thm not_less_zero}\<close>
+declare not_gr0[simp del] -- \<open>This is now @{thm not_gr_zero}\<close>
instance nat :: ordered_cancel_comm_monoid_add
proof qed