--- a/doc-src/TutorialI/Recdef/examples.thy Thu Mar 29 10:44:37 2001 +0200
+++ b/doc-src/TutorialI/Recdef/examples.thy Thu Mar 29 12:26:37 2001 +0200
@@ -79,7 +79,8 @@
text{*
Because of its pattern-matching syntax, \isacommand{recdef} is also useful
-for the definition of non-recursive functions:
+for the definition of non-recursive functions, where the termination measure
+degenerates to the empty set @{term"{}"}:
*}
consts swap12 :: "'a list \<Rightarrow> 'a list";
@@ -87,11 +88,6 @@
"swap12 (x#y#zs) = y#x#zs"
"swap12 zs = zs";
-text{*\noindent
-For non-recursive functions the termination measure degenerates to the empty
-set @{term"{}"}.
-*}
-
(*<*)
end
(*>*)