# HG changeset patch
# User krauss
# Date 1267465795 -3600
# Node ID 888993948a1ddc704245b5eead15a3eeccb753a6
# Parent  5f1ea533158cb7ab8983ebb584505e3b63df5c56
tuned comment

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