src/HOL/Nat.thy

--- a/src/HOL/Nat.thy	Sun Apr 24 21:31:14 2016 +0200
+++ b/src/HOL/Nat.thy	Mon Apr 25 16:09:26 2016 +0200
@@ -1832,7 +1832,7 @@
 proof -
   from assms obtain q where "m = n + Suc q"
     by (auto dest: less_imp_Suc_add)
-  moreover def r \<equiv> "Suc q"
+  moreover define r where "r = Suc q"
   ultimately have "Suc (m - Suc n) = r" and "m = n + r"
     by simp_all
   then show ?thesis by simp