updated

--- a/doc-src/IsarAdvanced/Functions/Thy/Functions.thy	Mon Nov 13 20:10:02 2006 +0100
+++ b/doc-src/IsarAdvanced/Functions/Thy/Functions.thy	Mon Nov 13 21:52:14 2006 +0100
@@ -24,8 +24,6 @@
 | "fib (Suc 0) = 1"
 | "fib (Suc (Suc n)) = fib n + fib (Suc n)"
 
-(*<*)termination by lexicographic_order(*>*)
-
 text {*
   The function always terminates, since the argument of gets smaller in every
   recursive call. Termination is an
@@ -55,7 +53,6 @@
 where
   "sep a (x#y#xs) = x # a # sep a (y # xs)"
 | "sep a xs       = xs"
-(*<*)termination by lexicographic_order(*>*)
 
 text {* 
   Overlapping patterns are interpreted as "increments" to what is
@@ -165,11 +162,11 @@
   @{text "N + 1 - i"} decreases in every recursive call.
 
   We can use this expression as a measure function to construct a
-  wellfounded relation, which is a proof of termination:
+  wellfounded relation, which can prove termination.
 *}
 
 termination 
-  by (auto_term "measure (\<lambda>(i,N). N + 1 - i)")
+  by (relation "measure (\<lambda>(i,N). N + 1 - i)") auto
 
 text {*
   Note that the two (curried) function arguments appear as a pair in
@@ -199,7 +196,7 @@
 *}
 
 termination 
-  by (auto_term "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]")
+  by (relation "measures [\<lambda>(i, N). N, \<lambda>(i,N). N + 1 - i]") auto
 
 
 section {* Mutual Recursion *}
@@ -208,7 +205,6 @@
   If two or more functions call one another mutually, they have to be defined
   in one step. The simplest example are probably @{text "even"} and @{text "odd"}:
 *}
-(*<*)hide const even odd(*>*)
 
 function even odd :: "nat \<Rightarrow> bool"
 where
@@ -228,7 +224,7 @@
 *}
 
 termination 
-  by (auto_term "measure (sum_case (%n. n) (%n. n))")
+  by (relation "measure (sum_case (%n. n) (%n. n))") auto
 
 
 

--- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Mon Nov 13 20:10:02 2006 +0100
+++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Mon Nov 13 21:52:14 2006 +0100
@@ -42,21 +42,7 @@
 \isakeyword{where}\isanewline
 \ \ {\isachardoublequoteopen}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
 {\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
-{\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ n\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
-%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
+{\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ n\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}%
 \begin{isamarkuptext}%
 The function always terminates, since the argument of gets smaller in every
   recursive call. Termination is an
@@ -90,19 +76,6 @@
 \isakeyword{where}\isanewline
 \ \ {\isachardoublequoteopen}sep\ a\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\ a\ {\isacharparenleft}y\ {\isacharhash}\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
 {\isacharbar}\ {\isachardoublequoteopen}sep\ a\ xs\ \ \ \ \ \ \ {\isacharequal}\ xs{\isachardoublequoteclose}%
-\isadelimproof
-%
-\endisadelimproof
-%
-\isatagproof
-%
-\endisatagproof
-{\isafoldproof}%
-%
-\isadelimproof
-%
-\endisadelimproof
-%
 \begin{isamarkuptext}%
 Overlapping patterns are interpreted as "increments" to what is
   already there: The second equation is only meant for the cases where
@@ -281,7 +254,7 @@
   \isa{N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i} decreases in every recursive call.
 
   We can use this expression as a measure function to construct a
-  wellfounded relation, which is a proof of termination:%
+  wellfounded relation, which can prove termination.%
 \end{isamarkuptext}%
 \isamarkuptrue%
 \isacommand{termination}\isamarkupfalse%
@@ -293,7 +266,7 @@
 %
 \isatagproof
 \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}i{\isacharcomma}N{\isacharparenright}{\isachardot}\ N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
+\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}i{\isacharcomma}N{\isacharparenright}{\isachardot}\ N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ auto%
 \endisatagproof
 {\isafoldproof}%
 %
@@ -351,7 +324,7 @@
 %
 \isatagproof
 \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}measures\ {\isacharbrackleft}{\isasymlambda}{\isacharparenleft}i{\isacharcomma}\ N{\isacharparenright}{\isachardot}\ N{\isacharcomma}\ {\isasymlambda}{\isacharparenleft}i{\isacharcomma}N{\isacharparenright}{\isachardot}\ N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i{\isacharbrackright}{\isachardoublequoteclose}{\isacharparenright}%
+\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measures\ {\isacharbrackleft}{\isasymlambda}{\isacharparenleft}i{\isacharcomma}\ N{\isacharparenright}{\isachardot}\ N{\isacharcomma}\ {\isasymlambda}{\isacharparenleft}i{\isacharcomma}N{\isacharparenright}{\isachardot}\ N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i{\isacharbrackright}{\isachardoublequoteclose}{\isacharparenright}\ auto%
 \endisatagproof
 {\isafoldproof}%
 %
@@ -368,7 +341,6 @@
   in one step. The simplest example are probably \isa{even} and \isa{odd}:%
 \end{isamarkuptext}%
 \isamarkuptrue%
-\isanewline
 \isacommand{function}\isamarkupfalse%
 \ even\ odd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
 \isakeyword{where}\isanewline
@@ -409,7 +381,7 @@
 %
 \isatagproof
 \isacommand{by}\isamarkupfalse%
-\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}measure\ {\isacharparenleft}sum{\isacharunderscore}case\ {\isacharparenleft}{\isacharpercent}n{\isachardot}\ n{\isacharparenright}\ {\isacharparenleft}{\isacharpercent}n{\isachardot}\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
+\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}sum{\isacharunderscore}case\ {\isacharparenleft}{\isacharpercent}n{\isachardot}\ n{\isacharparenright}\ {\isacharparenleft}{\isacharpercent}n{\isachardot}\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ auto%
 \endisatagproof
 {\isafoldproof}%
 %