--- a/src/HOL/Induct/Tree.thy Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Induct/Tree.thy Fri Nov 17 02:20:03 2006 +0100
@@ -72,10 +72,11 @@
closure. *}
definition
- brouwer_pred :: "(brouwer * brouwer) set"
+ brouwer_pred :: "(brouwer * brouwer) set" where
"brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})"
- brouwer_order :: "(brouwer * brouwer) set"
+definition
+ brouwer_order :: "(brouwer * brouwer) set" where
"brouwer_order = brouwer_pred^+"
lemma wf_brouwer_pred: "wf brouwer_pred"