1.1 --- a/src/HOL/Induct/Tree.thy	Sat May 27 17:42:00 2006 +0200
     1.2 +++ b/src/HOL/Induct/Tree.thy	Sat May 27 17:42:02 2006 +0200
     1.3 @@ -71,12 +71,12 @@
     1.4    ordinals.  Start with a predecessor relation and form its transitive 
     1.5    closure. *} 
     1.6  
     1.7 -constdefs
     1.8 +definition
     1.9    brouwer_pred :: "(brouwer * brouwer) set"
    1.10 -  "brouwer_pred == \<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)}"
    1.11 +  "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})"
    1.12  
    1.13    brouwer_order :: "(brouwer * brouwer) set"
    1.14 -  "brouwer_order == brouwer_pred^+"
    1.15 +  "brouwer_order = brouwer_pred^+"
    1.16  
    1.17  lemma wf_brouwer_pred: "wf brouwer_pred"
    1.18    by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+)