1.1 --- a/doc-src/TutorialI/Recdef/termination.thy	Wed Jan 24 11:59:15 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Recdef/termination.thy	Wed Jan 24 12:29:10 2001 +0100
     1.3 @@ -32,7 +32,7 @@
     1.4  lemma termi_lem: "\<not> x \<le> y \<Longrightarrow> x - Suc y < x - y";
     1.5  
     1.6  txt{*\noindent
     1.7 -It was not proved automatically because of the special nature of @{text"-"}
     1.8 +It was not proved automatically because of the special nature of subtraction
     1.9  on @{typ"nat"}. This requires more arithmetic than is tried by default:
    1.10  *}
    1.11