| changeset 10971 | 6852682eaf16 |
| parent 10795 | 9e888d60d3e5 |
| child 11309 | d666f11ca2d4 |
--- a/doc-src/TutorialI/Recdef/termination.thy Wed Jan 24 11:59:15 2001 +0100 +++ b/doc-src/TutorialI/Recdef/termination.thy Wed Jan 24 12:29:10 2001 +0100 @@ -32,7 +32,7 @@ lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y"; txt{*\noindent -It was not proved automatically because of the special nature of @{text"-"} +It was not proved automatically because of the special nature of subtraction on @{typ"nat"}. This requires more arithmetic than is tried by default: *}