--- a/doc-src/TutorialI/Advanced/Partial.thy Fri May 04 15:38:48 2001 +0200
+++ b/doc-src/TutorialI/Advanced/Partial.thy Fri May 04 15:39:38 2001 +0200
@@ -95,7 +95,7 @@
"find(f,x) = (if wf(step1 f)
then if f x = x then x else find(f, f x)
else arbitrary)"
-(hints recdef_simp:same_fst_def step1_def)
+(hints recdef_simp: step1_def)
text{*\noindent
The recursion equation itself should be clear enough: it is our aborted
@@ -115,8 +115,8 @@
well-foundedness of the relation given to \isacommand{recdef} is immediate.
Furthermore, each recursive call descends along that relation: the first
argument stays unchanged and the second one descends along @{term"step1
-f"}. The proof merely requires unfolding of some definitions, as specified in
-the \isacommand{hints} above.
+f"}. The proof requires unfolding the definition of @{term step1},
+as specified in the \isacommand{hints} above.
Normally you will then derive the following conditional variant of and from
the recursion equation
--- a/doc-src/TutorialI/Advanced/document/Partial.tex Fri May 04 15:38:48 2001 +0200
+++ b/doc-src/TutorialI/Advanced/document/Partial.tex Fri May 04 15:39:38 2001 +0200
@@ -98,7 +98,7 @@
\ \ {\isachardoublequote}find{\isacharparenleft}f{\isacharcomma}x{\isacharparenright}\ {\isacharequal}\ {\isacharparenleft}if\ wf{\isacharparenleft}step{\isadigit{1}}\ f{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ then\ if\ f\ x\ {\isacharequal}\ x\ then\ x\ else\ find{\isacharparenleft}f{\isacharcomma}\ f\ x{\isacharparenright}\isanewline
\ \ \ \ \ \ \ \ \ \ \ \ \ \ \ \ else\ arbitrary{\isacharparenright}{\isachardoublequote}\isanewline
-{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}same{\isacharunderscore}fst{\isacharunderscore}def\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
+{\isacharparenleft}\isakeyword{hints}\ recdef{\isacharunderscore}simp{\isacharcolon}\ step{\isadigit{1}}{\isacharunderscore}def{\isacharparenright}%
\begin{isamarkuptext}%
\noindent
The recursion equation itself should be clear enough: it is our aborted
@@ -123,8 +123,8 @@
is known to the well-foundedness prover of \isacommand{recdef}. Thus
well-foundedness of the relation given to \isacommand{recdef} is immediate.
Furthermore, each recursive call descends along that relation: the first
-argument stays unchanged and the second one descends along \isa{step{\isadigit{1}}\ f}. The proof merely requires unfolding of some definitions, as specified in
-the \isacommand{hints} above.
+argument stays unchanged and the second one descends along \isa{step{\isadigit{1}}\ f}. The proof requires unfolding the definition of \isa{step{\isadigit{1}}},
+as specified in the \isacommand{hints} above.
Normally you will then derive the following conditional variant of and from
the recursion equation%