--- a/doc-src/TutorialI/Recdef/document/Nested1.tex Mon Sep 11 17:59:53 2000 +0200
+++ b/doc-src/TutorialI/Recdef/document/Nested1.tex Mon Sep 11 18:00:47 2000 +0200
@@ -1,5 +1,6 @@
%
\begin{isabellebody}%
+\def\isabellecontext{Nested1}%
\isacommand{consts}\ trev\ \ {\isacharcolon}{\isacharcolon}\ {\isachardoublequote}{\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term\ {\isasymRightarrow}\ {\isacharparenleft}{\isacharprime}a{\isacharcomma}{\isacharprime}b{\isacharparenright}term{\isachardoublequote}%
\begin{isamarkuptext}%
\noindent
@@ -20,11 +21,9 @@
Remember that function \isa{size} is defined for each \isacommand{datatype}.
However, the definition does not succeed. Isabelle complains about an
unproved termination condition
-%
\begin{isabelle}%
\ \ \ \ \ t\ {\isasymin}\ set\ ts\ {\isasymlongrightarrow}\ size\ t\ {\isacharless}\ Suc\ {\isacharparenleft}term{\isacharunderscore}list{\isacharunderscore}size\ ts{\isacharparenright}%
-\end{isabelle}%
-
+\end{isabelle}
where \isa{set} returns the set of elements of a list (no special
knowledge of sets is required in the following) and \isa{term{\isacharunderscore}list{\isacharunderscore}size\ {\isacharcolon}{\isacharcolon}\ term\ list\ {\isasymRightarrow}\ nat} is an auxiliary function automatically defined by Isabelle
(when \isa{term} was defined). First we have to understand why the