1.1 --- a/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Mon May 12 22:11:06 2008 +0200
     1.2 +++ b/doc-src/IsarAdvanced/Functions/Thy/document/Functions.tex	Mon May 12 23:01:13 2008 +0200
     1.3 @@ -318,7 +318,7 @@
     1.4    these are packed together into a tuple, as it happened in the above
     1.5    example.
     1.6  
     1.7 -  The predefined function \isa{measure{\isasymColon}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a{\isacharparenright}\ set} constructs a
     1.8 +  The predefined function \isa{measure{\isasymColon}{\isacharparenleft}{\isacharprime}a\ {\isasymRightarrow}\ nat{\isacharparenright}\ {\isasymRightarrow}\ {\isacharprime}a\ {\isasymtimes}\ {\isacharprime}a\ {\isasymRightarrow}\ bool} constructs a
     1.9    wellfounded relation from a mapping into the natural numbers (a
    1.10    \emph{measure function}). 
    1.11  
    1.12 @@ -833,7 +833,7 @@
    1.13  
    1.14    This is an arithmetic triviality, but unfortunately the
    1.15    \isa{arith} method cannot handle this specific form of an
    1.16 -  elimination rule. However, we can use the method \isa{elim{\isacharunderscore}to{\isacharunderscore}cases} to do an ad-hoc conversion to a disjunction of
    1.17 +  elimination rule. However, we can use the method \isa{atomize{\isacharunderscore}elim} to do an ad-hoc conversion to a disjunction of
    1.18    existentials, which can then be soved by the arithmetic decision procedure.
    1.19    Pattern compatibility and termination are automatic as usual.%
    1.20  \end{isamarkuptxt}%
    1.21 @@ -865,7 +865,7 @@
    1.22  %
    1.23  \isatagproof
    1.24  \isacommand{apply}\isamarkupfalse%
    1.25 -\ elim{\isacharunderscore}to{\isacharunderscore}cases\isanewline
    1.26 +\ atomize{\isacharunderscore}elim\isanewline
    1.27  \isacommand{apply}\isamarkupfalse%
    1.28  \ arith\isanewline
    1.29  \isacommand{apply}\isamarkupfalse%
    1.30 @@ -913,7 +913,7 @@
    1.31  %
    1.32  \isatagproof
    1.33  \isacommand{apply}\isamarkupfalse%
    1.34 -\ elim{\isacharunderscore}to{\isacharunderscore}cases\isanewline
    1.35 +\ atomize{\isacharunderscore}elim\isanewline
    1.36  \isacommand{by}\isamarkupfalse%
    1.37  \ arith{\isacharplus}%
    1.38  \endisatagproof
    1.39 @@ -978,7 +978,7 @@
    1.40  %
    1.41  \isatagproof
    1.42  \isacommand{by}\isamarkupfalse%
    1.43 -\ {\isacharparenleft}elim{\isacharunderscore}to{\isacharunderscore}cases{\isacharcomma}\ auto{\isacharcomma}\ arith{\isacharparenright}%
    1.44 +\ {\isacharparenleft}atomize{\isacharunderscore}elim{\isacharcomma}\ auto{\isacharcomma}\ arith{\isacharparenright}%
    1.45  \endisatagproof
    1.46  {\isafoldproof}%
    1.47  %
    1.48 @@ -1792,8 +1792,11 @@
    1.49    list functions \isa{rev} and \isa{map}:%
    1.50  \end{isamarkuptext}%
    1.51  \isamarkuptrue%
    1.52 -\isacommand{lemma}\isamarkupfalse%
    1.53 -\ {\isacharbrackleft}simp{\isacharbrackright}{\isacharcolon}\ {\isachardoublequoteopen}x\ {\isasymin}\ set\ l\ {\isasymLongrightarrow}\ f\ x\ {\isacharless}\ Suc\ {\isacharparenleft}list{\isacharunderscore}size\ f\ l{\isacharparenright}{\isachardoublequoteclose}\isanewline
    1.54 +\isacommand{function}\isamarkupfalse%
    1.55 +\ mirror\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ tree{\isachardoublequoteclose}\isanewline
    1.56 +\isakeyword{where}\isanewline
    1.57 +\ \ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Leaf\ n{\isacharparenright}\ {\isacharequal}\ Leaf\ n{\isachardoublequoteclose}\isanewline
    1.58 +{\isacharbar}\ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Branch\ l{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}rev\ {\isacharparenleft}map\ mirror\ l{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}\isanewline
    1.59  %
    1.60  \isadelimproof
    1.61  %
    1.62 @@ -1801,21 +1804,14 @@
    1.63  %
    1.64  \isatagproof
    1.65  \isacommand{by}\isamarkupfalse%
    1.66 -\ {\isacharparenleft}induct\ l{\isacharparenright}\ auto%
    1.67 +\ pat{\isacharunderscore}completeness\ auto%
    1.68  \endisatagproof
    1.69  {\isafoldproof}%
    1.70  %
    1.71  \isadelimproof
    1.72 -\isanewline
    1.73  %
    1.74  \endisadelimproof
    1.75 -\isanewline
    1.76 -\isanewline
    1.77 -\isacommand{fun}\isamarkupfalse%
    1.78 -\ mirror\ {\isacharcolon}{\isacharcolon}\ {\isachardoublequoteopen}{\isacharprime}a\ tree\ {\isasymRightarrow}\ {\isacharprime}a\ tree{\isachardoublequoteclose}\isanewline
    1.79 -\isakeyword{where}\isanewline
    1.80 -\ \ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Leaf\ n{\isacharparenright}\ {\isacharequal}\ Leaf\ n{\isachardoublequoteclose}\isanewline
    1.81 -{\isacharbar}\ {\isachardoublequoteopen}mirror\ {\isacharparenleft}Branch\ l{\isacharparenright}\ {\isacharequal}\ Branch\ {\isacharparenleft}rev\ {\isacharparenleft}map\ mirror\ l{\isacharparenright}{\isacharparenright}{\isachardoublequoteclose}%
    1.82 +%
    1.83  \begin{isamarkuptext}%
    1.84  \emph{Note: The handling of size functions is currently changing 
    1.85    in the developers version of Isabelle. So this documentation is outdated.}%