src/HOL/Nat.thy
changeset 63040 eb4ddd18d635
parent 62683 ddd1c864408b
child 63099 af0e964aad7b
     1.1 --- a/src/HOL/Nat.thy	Sun Apr 24 21:31:14 2016 +0200
     1.2 +++ b/src/HOL/Nat.thy	Mon Apr 25 16:09:26 2016 +0200
     1.3 @@ -1832,7 +1832,7 @@
     1.4  proof -
     1.5    from assms obtain q where "m = n + Suc q"
     1.6      by (auto dest: less_imp_Suc_add)
     1.7 -  moreover def r \<equiv> "Suc q"
     1.8 +  moreover define r where "r = Suc q"
     1.9    ultimately have "Suc (m - Suc n) = r" and "m = n + r"
    1.10      by simp_all
    1.11    then show ?thesis by simp