author | krauss |
Mon, 01 Mar 2010 18:49:55 +0100 (2010-03-01) | |
changeset 35439 | 888993948a1d |
parent 35438 | 5f1ea533158c |
child 35440 | bdf8ad377877 |
--- 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. *}