1.1 --- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Mon Nov 13 20:10:02 2006 +0100
     1.2 +++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Mon Nov 13 21:52:14 2006 +0100
     1.3 @@ -42,21 +42,7 @@
     1.4  \isakeyword{where}\isanewline
     1.5  \ \ {\isachardoublequoteopen}fib\ {\isadigit{0}}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
     1.6  {\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isadigit{0}}{\isacharparenright}\ {\isacharequal}\ {\isadigit{1}}{\isachardoublequoteclose}\isanewline
     1.7 -{\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ n\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}\isanewline
     1.8 -%
     1.9 -\isadelimproof
    1.10 -%
    1.11 -\endisadelimproof
    1.12 -%
    1.13 -\isatagproof
    1.14 -%
    1.15 -\endisatagproof
    1.16 -{\isafoldproof}%
    1.17 -%
    1.18 -\isadelimproof
    1.19 -%
    1.20 -\endisadelimproof
    1.21 -%
    1.22 +{\isacharbar}\ {\isachardoublequoteopen}fib\ {\isacharparenleft}Suc\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isacharparenright}\ {\isacharequal}\ fib\ n\ {\isacharplus}\ fib\ {\isacharparenleft}Suc\ n{\isacharparenright}{\isachardoublequoteclose}%
    1.23  \begin{isamarkuptext}%
    1.24  The function always terminates, since the argument of gets smaller in every
    1.25    recursive call. Termination is an
    1.26 @@ -90,19 +76,6 @@
    1.27  \isakeyword{where}\isanewline
    1.28  \ \ {\isachardoublequoteopen}sep\ a\ {\isacharparenleft}x{\isacharhash}y{\isacharhash}xs{\isacharparenright}\ {\isacharequal}\ x\ {\isacharhash}\ a\ {\isacharhash}\ sep\ a\ {\isacharparenleft}y\ {\isacharhash}\ xs{\isacharparenright}{\isachardoublequoteclose}\isanewline
    1.29  {\isacharbar}\ {\isachardoublequoteopen}sep\ a\ xs\ \ \ \ \ \ \ {\isacharequal}\ xs{\isachardoublequoteclose}%
    1.30 -\isadelimproof
    1.31 -%
    1.32 -\endisadelimproof
    1.33 -%
    1.34 -\isatagproof
    1.35 -%
    1.36 -\endisatagproof
    1.37 -{\isafoldproof}%
    1.38 -%
    1.39 -\isadelimproof
    1.40 -%
    1.41 -\endisadelimproof
    1.42 -%
    1.43  \begin{isamarkuptext}%
    1.44  Overlapping patterns are interpreted as "increments" to what is
    1.45    already there: The second equation is only meant for the cases where
    1.46 @@ -281,7 +254,7 @@
    1.47    \isa{N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i} decreases in every recursive call.
    1.48  
    1.49    We can use this expression as a measure function to construct a
    1.50 -  wellfounded relation, which is a proof of termination:%
    1.51 +  wellfounded relation, which can prove termination.%
    1.52  \end{isamarkuptext}%
    1.53  \isamarkuptrue%
    1.54  \isacommand{termination}\isamarkupfalse%
    1.55 @@ -293,7 +266,7 @@
    1.56  %
    1.57  \isatagproof
    1.58  \isacommand{by}\isamarkupfalse%
    1.59 -\ {\isacharparenleft}auto{\isacharunderscore}term\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}i{\isacharcomma}N{\isacharparenright}{\isachardot}\ N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}%
    1.60 +\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}{\isasymlambda}{\isacharparenleft}i{\isacharcomma}N{\isacharparenright}{\isachardot}\ N\ {\isacharplus}\ {\isadigit{1}}\ {\isacharminus}\ i{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ auto%
    1.61  \endisatagproof
    1.62  {\isafoldproof}%
    1.63  %
    1.64 @@ -351,7 +324,7 @@
    1.65  %
    1.66  \isatagproof
    1.67  \isacommand{by}\isamarkupfalse%
    1.68 -\ {\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}%
    1.69 +\ {\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%
    1.70  \endisatagproof
    1.71  {\isafoldproof}%
    1.72  %
    1.73 @@ -368,7 +341,6 @@
    1.74    in one step. The simplest example are probably \isa{even} and \isa{odd}:%
    1.75  \end{isamarkuptext}%
    1.76  \isamarkuptrue%
    1.77 -\isanewline
    1.78  \isacommand{function}\isamarkupfalse%
    1.79  \ even\ odd\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}nat\ {\isasymRightarrow}\ bool{\isachardoublequoteclose}\isanewline
    1.80  \isakeyword{where}\isanewline
    1.81 @@ -409,7 +381,7 @@
    1.82  %
    1.83  \isatagproof
    1.84  \isacommand{by}\isamarkupfalse%
    1.85 -\ {\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}%
    1.86 +\ {\isacharparenleft}relation\ {\isachardoublequoteopen}measure\ {\isacharparenleft}sum{\isacharunderscore}case\ {\isacharparenleft}{\isacharpercent}n{\isachardot}\ n{\isacharparenright}\ {\isacharparenleft}{\isacharpercent}n{\isachardot}\ n{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}{\isacharparenright}\ auto%
    1.87  \endisatagproof
    1.88  {\isafoldproof}%
    1.89  %