--- 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.
*};