| changeset 67399 | eab6ce8368fa |
| parent 66952 | 80985b62029d |
| child 68259 | 80df7c90e315 |
--- a/src/HOL/Wellfounded.thy Wed Jan 10 15:21:49 2018 +0100 +++ b/src/HOL/Wellfounded.thy Wed Jan 10 15:25:09 2018 +0100 @@ -500,7 +500,7 @@ subsection \<open>@{typ nat} is well-founded\<close> -lemma less_nat_rel: "op < = (\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+" +lemma less_nat_rel: "(<) = (\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+" proof (rule ext, rule ext, rule iffI) fix n m :: nat show "(\<lambda>m n. n = Suc m)\<^sup>+\<^sup>+ m n" if "m < n"