src/HOL/Induct/Tree.thy
changeset 21404 eb85850d3eb7
parent 19736 d8d0f8f51d69
child 31602 59df8222c204
     1.1 --- a/src/HOL/Induct/Tree.thy	Fri Nov 17 02:19:55 2006 +0100
     1.2 +++ b/src/HOL/Induct/Tree.thy	Fri Nov 17 02:20:03 2006 +0100
     1.3 @@ -72,10 +72,11 @@
     1.4    closure. *} 
     1.5  
     1.6  definition
     1.7 -  brouwer_pred :: "(brouwer * brouwer) set"
     1.8 +  brouwer_pred :: "(brouwer * brouwer) set" where
     1.9    "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})"
    1.10  
    1.11 -  brouwer_order :: "(brouwer * brouwer) set"
    1.12 +definition
    1.13 +  brouwer_order :: "(brouwer * brouwer) set" where
    1.14    "brouwer_order = brouwer_pred^+"
    1.15  
    1.16  lemma wf_brouwer_pred: "wf brouwer_pred"