--- a/doc-src/TutorialI/Advanced/Partial.thy Thu Nov 29 20:02:23 2001 +0100
+++ b/doc-src/TutorialI/Advanced/Partial.thy Thu Nov 29 21:12:37 2001 +0100
@@ -146,9 +146,9 @@
text{*If the recursive function happens to be tail recursive, its
definition becomes a triviality if based on the predefined \cdx{while}
-combinator. The latter lives in the Library theory
-\thydx{While_Combinator}, which is not part of @{text Main} but needs to
-be included explicitly among the ancestor theories.
+combinator. The latter lives in the Library theory \thydx{While_Combinator}.
+% which is not part of {text Main} but needs to
+% be included explicitly among the ancestor theories.
Constant @{term while} is of type @{text"('a \<Rightarrow> bool) \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a"}
and satisfies the recursion equation @{thm[display]while_unfold[no_vars]}