--- a/doc-src/TutorialI/Recdef/termination.thy Wed Oct 11 00:03:22 2000 +0200
+++ b/doc-src/TutorialI/Recdef/termination.thy Wed Oct 11 09:09:06 2000 +0200
@@ -81,21 +81,6 @@
about @{term f}. In most cases this is more cumbersome than proving things
up front.
%FIXME, with one exception: nested recursion.
-
-Although all the above examples employ measure functions, \isacommand{recdef}
-allows arbitrary wellfounded relations. For example, termination of
-Ackermann's function requires the lexicographic product @{text"<*lex*>"}:
-*}
-
-consts ack :: "nat\<times>nat \<Rightarrow> nat";
-recdef ack "measure(\<lambda>m. m) <*lex*> measure(\<lambda>n. n)"
- "ack(0,n) = Suc n"
- "ack(Suc m,0) = ack(m, 1)"
- "ack(Suc m,Suc n) = ack(m,ack(Suc m,n))";
-
-text{*\noindent
-For details see the manual~\cite{isabelle-HOL} and the examples in the
-library.
*}
(*<*)