1.1 --- a/src/HOL/Induct/Tree.thy	Tue Mar 02 09:05:50 2010 +0100
     1.2 +++ b/src/HOL/Induct/Tree.thy	Mon Mar 01 18:49:55 2010 +0100
     1.3 @@ -68,7 +68,7 @@
     1.4  
     1.5  subsection{*A WF Ordering for The Brouwer ordinals (Michael Compton)*}
     1.6  
     1.7 -text{*To define recdef style functions we need an ordering on the Brouwer
     1.8 +text{*To use the function package we need an ordering on the Brouwer
     1.9    ordinals.  Start with a predecessor relation and form its transitive 
    1.10    closure. *} 
    1.11