doc-src/TutorialI/Advanced/advanced.tex
changeset 11196 bb4ede27fcb7
parent 10885 90695f46440b
child 11216 279004936bb0
     1.1 --- a/doc-src/TutorialI/Advanced/advanced.tex	Mon Mar 05 15:47:11 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Advanced/advanced.tex	Wed Mar 07 15:54:11 2001 +0100
     1.3 @@ -13,8 +13,8 @@
     1.4  \index{*recdef|(}
     1.5  
     1.6  The purpose of this section is to introduce advanced forms of
     1.7 -\isacommand{recdef}: how to define recursive function over nested recursive
     1.8 -datatypes, how to establish termination by means other than measure functions,
     1.9 +\isacommand{recdef}: how to establish termination by means other than measure
    1.10 +functions, how to define recursive function over nested recursive datatypes,
    1.11  and how to deal with partial functions.
    1.12  
    1.13  If, after reading this section, you feel that the definition of recursive
    1.14 @@ -27,16 +27,16 @@
    1.15  proof time. In HOL you may have to work hard to define a function, but proofs
    1.16  can then proceed unencumbered by worries about undefinedness.
    1.17  
    1.18 +\subsection{Beyond measure}
    1.19 +\label{sec:beyond-measure}
    1.20 +\input{Advanced/document/WFrec.tex}
    1.21 +
    1.22  \subsection{Recursion over nested datatypes}
    1.23  \label{sec:nested-recdef}
    1.24  \input{Recdef/document/Nested0.tex}
    1.25  \input{Recdef/document/Nested1.tex}
    1.26  \input{Recdef/document/Nested2.tex}
    1.27  
    1.28 -\subsection{Beyond measure}
    1.29 -\label{sec:beyond-measure}
    1.30 -\input{Advanced/document/WFrec.tex}
    1.31 -
    1.32  \subsection{Partial functions}
    1.33  \index{partial function}
    1.34  \input{Advanced/document/Partial.tex}