diff -r dd58f13a8eb4 -r eb85850d3eb7 src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Fri Nov 17 02:19:55 2006 +0100
+++ b/src/HOL/Hyperreal/NSA.thy	Fri Nov 17 02:20:03 2006 +0100
@@ -12,32 +12,37 @@
 begin
 
 definition
-
-  hnorm :: "'a::norm star \<Rightarrow> real star"
+  hnorm :: "'a::norm star \<Rightarrow> real star" where
   "hnorm = *f* norm"
 
-  Infinitesimal  :: "('a::real_normed_vector) star set"
+definition
+  Infinitesimal  :: "('a::real_normed_vector) star set" where
   "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
 
-  HFinite :: "('a::real_normed_vector) star set"
+definition
+  HFinite :: "('a::real_normed_vector) star set" where
   "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
 
-  HInfinite :: "('a::real_normed_vector) star set"
+definition
+  HInfinite :: "('a::real_normed_vector) star set" where
   "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
 
-  approx :: "['a::real_normed_vector star, 'a star] => bool"
-    (infixl "@=" 50)
+definition
+  approx :: "['a::real_normed_vector star, 'a star] => bool"  (infixl "@=" 50) where
     --{*the `infinitely close' relation*}
   "(x @= y) = ((x - y) \<in> Infinitesimal)"
 
-  st        :: "hypreal => hypreal"
+definition
+  st        :: "hypreal => hypreal" where
     --{*the standard part of a hyperreal*}
   "st = (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"
 
-  monad     :: "'a::real_normed_vector star => 'a star set"
+definition
+  monad     :: "'a::real_normed_vector star => 'a star set" where
   "monad x = {y. x @= y}"
 
-  galaxy    :: "'a::real_normed_vector star => 'a star set"
+definition
+  galaxy    :: "'a::real_normed_vector star => 'a star set" where
   "galaxy x = {y. (x + -y) \<in> HFinite}"
 
 notation (xsymbols)
@@ -52,7 +57,7 @@
 subsection {* Nonstandard Extension of the Norm Function *}
 
 definition
-  scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star"
+  scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star" where
   "scaleHR = starfun2 scaleR"
 
 declare hnorm_def [transfer_unfold]