diff -r 65ede8dfe304 -r bb4ede27fcb7 doc-src/TutorialI/Advanced/WFrec.thy
--- a/doc-src/TutorialI/Advanced/WFrec.thy	Mon Mar 05 15:47:11 2001 +0100
+++ b/doc-src/TutorialI/Advanced/WFrec.thy	Wed Mar 07 15:54:11 2001 +0100
@@ -32,7 +32,7 @@
 
 Each \isacommand{recdef} definition should be accompanied (after the name of
 the function) by a well-founded relation on the argument type of the
-function.  HOL formalizes some of the most important
+function.  Isabelle/HOL formalizes some of the most important
 constructions of well-founded relations (see \S\ref{sec:Well-founded}). For
 example, @{term"measure f"} is always well-founded, and the lexicographic
 product of two well-founded relations is again well-founded, which we relied
@@ -77,7 +77,7 @@
 
 lemma wf_greater: "wf {(i,j). j<i \<and> i \<le> (N::nat)}"
 
-txt{*
+txt{*\noindent
 The proof is by showing that our relation is a subset of another well-founded
 relation: one given by a measure function. 
 *};