diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/FixedPoint.thy
--- a/src/HOL/FixedPoint.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/FixedPoint.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -20,12 +20,13 @@
 defs Sup_def: "Sup A == Meet {b. \<forall>a \<in> A. a <= b}"
 
 definition
- SUP :: "('a \<Rightarrow> 'b::order) \<Rightarrow> 'b" (binder "SUP " 10)
-"SUP x. f x == Sup (f ` UNIV)"
+  SUP :: "('a \<Rightarrow> 'b::order) \<Rightarrow> 'b"  (binder "SUP " 10) where
+  "SUP x. f x == Sup (f ` UNIV)"
+
 (*
 abbreviation
- bot :: "'a::order"
-"bot == Sup {}"
+  bot :: "'a::order" where
+  "bot == Sup {}"
 *)
 axclass comp_lat < order
   Meet_lower: "x \<in> A \<Longrightarrow> Meet A <= x"