| changeset 69605 | a96320074298 |
| parent 69593 | 3dda49e08b9d |
| child 69661 | a03a63b81f44 |
--- a/src/HOL/Nat.thy Sun Jan 06 13:44:33 2019 +0100 +++ b/src/HOL/Nat.thy Sun Jan 06 15:04:34 2019 +0100 @@ -1930,7 +1930,7 @@ shows "u = s" using assms(2,1) by (rule trans) -ML_file "Tools/nat_arith.ML" +ML_file \<open>Tools/nat_arith.ML\<close> simproc_setup nateq_cancel_sums ("(l::nat) + m = n" | "(l::nat) = m + n" | "Suc m = n" | "m = Suc n") =