diff -r 7917e66505a4 -r 6852682eaf16 doc-src/TutorialI/Recdef/termination.thy
--- 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:
 *}