src/HOL/Induct/Tree.thy
changeset 19736 d8d0f8f51d69
parent 18242 2215049cd29c
child 21404 eb85850d3eb7
--- a/src/HOL/Induct/Tree.thy	Sat May 27 17:42:00 2006 +0200
+++ b/src/HOL/Induct/Tree.thy	Sat May 27 17:42:02 2006 +0200
@@ -71,12 +71,12 @@
   ordinals.  Start with a predecessor relation and form its transitive 
   closure. *} 
 
-constdefs
+definition
   brouwer_pred :: "(brouwer * brouwer) set"
-  "brouwer_pred == \<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)}"
+  "brouwer_pred = (\<Union>i. {(m,n). n = Succ m \<or> (EX f. n = Lim f & m = f i)})"
 
   brouwer_order :: "(brouwer * brouwer) set"
-  "brouwer_order == brouwer_pred^+"
+  "brouwer_order = brouwer_pred^+"
 
 lemma wf_brouwer_pred: "wf brouwer_pred"
   by(unfold wf_def brouwer_pred_def, clarify, induct_tac x, blast+)