1.1 --- a/doc-src/TutorialI/Inductive/even-example.tex	Fri Mar 09 19:05:48 2001 +0100
     1.2 +++ b/doc-src/TutorialI/Inductive/even-example.tex	Mon Mar 12 18:17:45 2001 +0100
     1.3 @@ -25,7 +25,9 @@
     1.4  An inductive definition consists of introduction rules.  The first one
     1.5  above states that 0 is even; the second states that if $n$ is even, then so
     1.6  is~$n+2$.  Given this declaration, Isabelle generates a fixed point
     1.7 -definition for \isa{even} and proves theorems about it.  These theorems
     1.8 +definition for \isa{even} and proves theorems about it,
     1.9 +thus following the definitional approach (see \S\ref{sec:definitional}).
    1.10 +These theorems
    1.11  include the introduction rules specified in the declaration, an elimination
    1.12  rule for case analysis and an induction rule.  We can refer to these
    1.13  theorems by automatically-generated names.  Here are two examples:

     2.1 --- a/doc-src/TutorialI/fp.tex	Fri Mar 09 19:05:48 2001 +0100
     2.2 +++ b/doc-src/TutorialI/fp.tex	Mon Mar 12 18:17:45 2001 +0100
     2.3 @@ -269,6 +269,26 @@
     2.4  \input{Misc/document/prime_def.tex}
     2.5  
     2.6  
     2.7 +\section{The Definitional Approach}
     2.8 +\label{sec:definitional}
     2.9 +
    2.10 +As we pointed out at the beginning of the chapter, asserting arbitrary
    2.11 +axioms, e.g. $f(n) = f(n) + 1$, may easily lead to contradictions. In order
    2.12 +to avoid this danger, this tutorial advocates the definitional rather than
    2.13 +the axiomatic approach: introduce new concepts by definitions, thus
    2.14 +preserving consistency. However, on the face of it, Isabelle/HOL seems to
    2.15 +support many more constructs than just definitions, for example
    2.16 +\isacommand{primrec}. The crucial point is that internally, everything
    2.17 +(except real axioms) is reduced to a definition. For example, given some
    2.18 +\isacommand{primrec} function definition, this is turned into a proper
    2.19 +(nonrecursive!) definition, and the user-supplied recursion equations are
    2.20 +derived as theorems from the definition. This tricky process is completely
    2.21 +hidden from the user and it is not necessary to understand the details. The
    2.22 +result of the definitional approach is that \isacommand{primrec} is as safe
    2.23 +as pure \isacommand{defs} are, but more convenient. And this is not just the
    2.24 +case for \isacommand{primrec} but also for the other commands described
    2.25 +later, like \isacommand{recdef} and \isacommand{inductive}.
    2.26 +
    2.27  \chapter{More Functional Programming}
    2.28  
    2.29  The purpose of this chapter is to deepen the reader's understanding of the

     3.1 --- a/doc-src/TutorialI/todo.tobias	Fri Mar 09 19:05:48 2001 +0100
     3.2 +++ b/doc-src/TutorialI/todo.tobias	Mon Mar 12 18:17:45 2001 +0100
     3.3 @@ -57,8 +57,6 @@
     3.4  
     3.5  Advanced recdef: explain recdef_tc?
     3.6  
     3.7 -say something about definitional approach. In recdef section? At the end?
     3.8 -
     3.9  I guess we should say "HOL" everywhere, with a remark early on about the
    3.10  differences between our HOL and the other one.
    3.11