# HG changeset patch
# User nipkow
# Date 988983578 -7200
# Node ID 3826c51d980e8ef690e833c50b81be0fa7e6836e
# Parent  981ea92a86dd603593715e02cd966e366b841531
*** empty log message ***

diff -r 981ea92a86dd -r 3826c51d980e doc-src/TutorialI/Advanced/Partial.thy
--- 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
diff -r 981ea92a86dd -r 3826c51d980e doc-src/TutorialI/Advanced/document/Partial.tex
--- 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%