# HG changeset patch
# User wenzelm
# Date 1149283349 -7200
# Node ID dfe9409116178648504b9225aa3355fa0ba38ba4
# Parent  372065f34795551e788f69902aa2a9feafd6b6f3
misc cleanup;

diff -r 372065f34795 -r dfe940911617 src/HOL/Complex/CLim.thy
--- a/src/HOL/Complex/CLim.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Complex/CLim.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -33,79 +33,79 @@
 apply (drule sym [THEN diff_eq_eq [THEN iffD2]], auto)
 done
 
-constdefs
+definition
 
   CLIM :: "[complex=>complex,complex,complex] => bool"
 				("((_)/ -- (_)/ --C> (_))" [60, 0, 60] 60)
-  "f -- a --C> L ==
-     \<forall>r. 0 < r -->
+  "f -- a --C> L =
+     (\<forall>r. 0 < r -->
 	     (\<exists>s. 0 < s & (\<forall>x. (x \<noteq> a & (cmod(x - a) < s)
-			  --> cmod(f x - L) < r)))"
+			  --> cmod(f x - L) < r))))"
 
   NSCLIM :: "[complex=>complex,complex,complex] => bool"
 			      ("((_)/ -- (_)/ --NSC> (_))" [60, 0, 60] 60)
-  "f -- a --NSC> L == (\<forall>x. (x \<noteq> hcomplex_of_complex a &
+  "f -- a --NSC> L = (\<forall>x. (x \<noteq> hcomplex_of_complex a &
            		         x @c= hcomplex_of_complex a
                                    --> ( *f* f) x @c= hcomplex_of_complex L))"
 
   (* f: C --> R *)
   CRLIM :: "[complex=>real,complex,real] => bool"
 				("((_)/ -- (_)/ --CR> (_))" [60, 0, 60] 60)
-  "f -- a --CR> L ==
-     \<forall>r. 0 < r -->
+  "f -- a --CR> L =
+     (\<forall>r. 0 < r -->
 	     (\<exists>s. 0 < s & (\<forall>x. (x \<noteq> a & (cmod(x - a) < s)
-			  --> abs(f x - L) < r)))"
+			  --> abs(f x - L) < r))))"
 
   NSCRLIM :: "[complex=>real,complex,real] => bool"
 			      ("((_)/ -- (_)/ --NSCR> (_))" [60, 0, 60] 60)
-  "f -- a --NSCR> L == (\<forall>x. (x \<noteq> hcomplex_of_complex a &
+  "f -- a --NSCR> L = (\<forall>x. (x \<noteq> hcomplex_of_complex a &
            		         x @c= hcomplex_of_complex a
                                    --> ( *f* f) x @= hypreal_of_real L))"
 
 
   isContc :: "[complex=>complex,complex] => bool"
-  "isContc f a == (f -- a --C> (f a))"
+  "isContc f a = (f -- a --C> (f a))"
 
   (* NS definition dispenses with limit notions *)
   isNSContc :: "[complex=>complex,complex] => bool"
-  "isNSContc f a == (\<forall>y. y @c= hcomplex_of_complex a -->
+  "isNSContc f a = (\<forall>y. y @c= hcomplex_of_complex a -->
 			   ( *f* f) y @c= hcomplex_of_complex (f a))"
 
   isContCR :: "[complex=>real,complex] => bool"
-  "isContCR f a == (f -- a --CR> (f a))"
+  "isContCR f a = (f -- a --CR> (f a))"
 
   (* NS definition dispenses with limit notions *)
   isNSContCR :: "[complex=>real,complex] => bool"
-  "isNSContCR f a == (\<forall>y. y @c= hcomplex_of_complex a -->
+  "isNSContCR f a = (\<forall>y. y @c= hcomplex_of_complex a -->
 			   ( *f* f) y @= hypreal_of_real (f a))"
 
   (* differentiation: D is derivative of function f at x *)
   cderiv:: "[complex=>complex,complex,complex] => bool"
 			    ("(CDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
-  "CDERIV f x :> D == ((%h. (f(x + h) - f(x))/h) -- 0 --C> D)"
+  "CDERIV f x :> D = ((%h. (f(x + h) - f(x))/h) -- 0 --C> D)"
 
   nscderiv :: "[complex=>complex,complex,complex] => bool"
 			    ("(NSCDERIV (_)/ (_)/ :> (_))" [60, 0, 60] 60)
-  "NSCDERIV f x :> D == (\<forall>h \<in> CInfinitesimal - {0}.
+  "NSCDERIV f x :> D = (\<forall>h \<in> CInfinitesimal - {0}.
 			      (( *f* f)(hcomplex_of_complex x + h)
         			 - hcomplex_of_complex (f x))/h @c= hcomplex_of_complex D)"
 
   cdifferentiable :: "[complex=>complex,complex] => bool"
                      (infixl "cdifferentiable" 60)
-  "f cdifferentiable x == (\<exists>D. CDERIV f x :> D)"
+  "f cdifferentiable x = (\<exists>D. CDERIV f x :> D)"
 
   NSCdifferentiable :: "[complex=>complex,complex] => bool"
                         (infixl "NSCdifferentiable" 60)
-  "f NSCdifferentiable x == (\<exists>D. NSCDERIV f x :> D)"
+  "f NSCdifferentiable x = (\<exists>D. NSCDERIV f x :> D)"
 
 
   isUContc :: "(complex=>complex) => bool"
-  "isUContc f ==  (\<forall>r. 0 < r -->
+  "isUContc f =  (\<forall>r. 0 < r -->
 		      (\<exists>s. 0 < s & (\<forall>x y. cmod(x - y) < s
 			    --> cmod(f x - f y) < r)))"
 
   isNSUContc :: "(complex=>complex) => bool"
-  "isNSUContc f == (\<forall>x y. x @c= y --> ( *f* f) x @c= ( *f* f) y)"
+  "isNSUContc f = (\<forall>x y. x @c= y --> ( *f* f) x @c= ( *f* f) y)"
 
 
 
@@ -1020,156 +1020,4 @@
       ==> NSCDERIV f x :> l"
 by (auto simp add: NSCDERIV_iff2 isNSContc_def cstarfun_if_eq); 
 
-
-ML
-{*
-val complex_add_minus_iff = thm "complex_add_minus_iff";
-val complex_add_eq_0_iff = thm "complex_add_eq_0_iff";
-val NSCLIM_NSCRLIM_Re = thm "NSCLIM_NSCRLIM_Re";
-val NSCLIM_NSCRLIM_Im = thm "NSCLIM_NSCRLIM_Im";
-val CLIM_NSCLIM = thm "CLIM_NSCLIM";
-val eq_Abs_star_ALL = thm "eq_Abs_star_ALL";
-val lemma_CLIM = thm "lemma_CLIM";
-val lemma_skolemize_CLIM2 = thm "lemma_skolemize_CLIM2";
-val lemma_csimp = thm "lemma_csimp";
-val NSCLIM_CLIM = thm "NSCLIM_CLIM";
-val CLIM_NSCLIM_iff = thm "CLIM_NSCLIM_iff";
-val CRLIM_NSCRLIM = thm "CRLIM_NSCRLIM";
-val lemma_CRLIM = thm "lemma_CRLIM";
-val lemma_skolemize_CRLIM2 = thm "lemma_skolemize_CRLIM2";
-val lemma_crsimp = thm "lemma_crsimp";
-val NSCRLIM_CRLIM = thm "NSCRLIM_CRLIM";
-val CRLIM_NSCRLIM_iff = thm "CRLIM_NSCRLIM_iff";
-val CLIM_CRLIM_Re = thm "CLIM_CRLIM_Re";
-val CLIM_CRLIM_Im = thm "CLIM_CRLIM_Im";
-val CLIM_cnj = thm "CLIM_cnj";
-val CLIM_cnj_iff = thm "CLIM_cnj_iff";
-val NSCLIM_add = thm "NSCLIM_add";
-val CLIM_add = thm "CLIM_add";
-val NSCLIM_mult = thm "NSCLIM_mult";
-val CLIM_mult = thm "CLIM_mult";
-val NSCLIM_const = thm "NSCLIM_const";
-val CLIM_const = thm "CLIM_const";
-val NSCLIM_minus = thm "NSCLIM_minus";
-val CLIM_minus = thm "CLIM_minus";
-val NSCLIM_diff = thm "NSCLIM_diff";
-val CLIM_diff = thm "CLIM_diff";
-val NSCLIM_inverse = thm "NSCLIM_inverse";
-val CLIM_inverse = thm "CLIM_inverse";
-val NSCLIM_zero = thm "NSCLIM_zero";
-val CLIM_zero = thm "CLIM_zero";
-val NSCLIM_zero_cancel = thm "NSCLIM_zero_cancel";
-val CLIM_zero_cancel = thm "CLIM_zero_cancel";
-val NSCLIM_not_zero = thm "NSCLIM_not_zero";
-val NSCLIM_not_zeroE = thms "NSCLIM_not_zeroE";
-val CLIM_not_zero = thm "CLIM_not_zero";
-val NSCLIM_const_eq = thm "NSCLIM_const_eq";
-val CLIM_const_eq = thm "CLIM_const_eq";
-val NSCLIM_unique = thm "NSCLIM_unique";
-val CLIM_unique = thm "CLIM_unique";
-val NSCLIM_mult_zero = thm "NSCLIM_mult_zero";
-val CLIM_mult_zero = thm "CLIM_mult_zero";
-val NSCLIM_self = thm "NSCLIM_self";
-val CLIM_self = thm "CLIM_self";
-val NSCLIM_NSCRLIM_iff = thm "NSCLIM_NSCRLIM_iff";
-val CLIM_CRLIM_iff = thm "CLIM_CRLIM_iff";
-val NSCLIM_NSCRLIM_iff2 = thm "NSCLIM_NSCRLIM_iff2";
-val NSCLIM_NSCRLIM_Re_Im_iff = thm "NSCLIM_NSCRLIM_Re_Im_iff";
-val CLIM_CRLIM_Re_Im_iff = thm "CLIM_CRLIM_Re_Im_iff";
-val isNSContcD = thm "isNSContcD";
-val isNSContc_NSCLIM = thm "isNSContc_NSCLIM";
-val NSCLIM_isNSContc = thm "NSCLIM_isNSContc";
-val isNSContc_NSCLIM_iff = thm "isNSContc_NSCLIM_iff";
-val isNSContc_CLIM_iff = thm "isNSContc_CLIM_iff";
-val isNSContc_isContc_iff = thm "isNSContc_isContc_iff";
-val isContc_isNSContc = thm "isContc_isNSContc";
-val isNSContc_isContc = thm "isNSContc_isContc";
-val NSCLIM_h_iff = thm "NSCLIM_h_iff";
-val NSCLIM_isContc_iff = thm "NSCLIM_isContc_iff";
-val CLIM_isContc_iff = thm "CLIM_isContc_iff";
-val isContc_iff = thm "isContc_iff";
-val isContc_add = thm "isContc_add";
-val isContc_mult = thm "isContc_mult";
-val isContc_o = thm "isContc_o";
-val isContc_o2 = thm "isContc_o2";
-val isNSContc_minus = thm "isNSContc_minus";
-val isContc_minus = thm "isContc_minus";
-val isContc_inverse = thm "isContc_inverse";
-val isNSContc_inverse = thm "isNSContc_inverse";
-val isContc_diff = thm "isContc_diff";
-val isContc_const = thm "isContc_const";
-val isNSContc_const = thm "isNSContc_const";
-val isNSContCRD = thm "isNSContCRD";
-val isNSContCR_NSCRLIM = thm "isNSContCR_NSCRLIM";
-val NSCRLIM_isNSContCR = thm "NSCRLIM_isNSContCR";
-val isNSContCR_NSCRLIM_iff = thm "isNSContCR_NSCRLIM_iff";
-val isNSContCR_CRLIM_iff = thm "isNSContCR_CRLIM_iff";
-val isNSContCR_isContCR_iff = thm "isNSContCR_isContCR_iff";
-val isContCR_isNSContCR = thm "isContCR_isNSContCR";
-val isNSContCR_isContCR = thm "isNSContCR_isContCR";
-val isNSContCR_cmod = thm "isNSContCR_cmod";
-val isContCR_cmod = thm "isContCR_cmod";
-val isContc_isContCR_Re = thm "isContc_isContCR_Re";
-val isContc_isContCR_Im = thm "isContc_isContCR_Im";
-val CDERIV_iff = thm "CDERIV_iff";
-val CDERIV_NSC_iff = thm "CDERIV_NSC_iff";
-val CDERIVD = thm "CDERIVD";
-val NSC_DERIVD = thm "NSC_DERIVD";
-val CDERIV_unique = thm "CDERIV_unique";
-val NSCDeriv_unique = thm "NSCDeriv_unique";
-val CDERIV_CLIM_iff = thm "CDERIV_CLIM_iff";
-val CDERIV_iff2 = thm "CDERIV_iff2";
-val NSCDERIV_NSCLIM_iff = thm "NSCDERIV_NSCLIM_iff";
-val NSCDERIV_NSCLIM_iff2 = thm "NSCDERIV_NSCLIM_iff2";
-val NSCDERIV_iff2 = thm "NSCDERIV_iff2";
-val NSCDERIV_CDERIV_iff = thm "NSCDERIV_CDERIV_iff";
-val NSCDERIV_isNSContc = thm "NSCDERIV_isNSContc";
-val CDERIV_isContc = thm "CDERIV_isContc";
-val NSCDERIV_const = thm "NSCDERIV_const";
-val CDERIV_const = thm "CDERIV_const";
-val NSCDERIV_add = thm "NSCDERIV_add";
-val CDERIV_add = thm "CDERIV_add";
-val lemma_nscderiv1 = thm "lemma_nscderiv1";
-val lemma_nscderiv2 = thm "lemma_nscderiv2";
-val NSCDERIV_mult = thm "NSCDERIV_mult";
-val CDERIV_mult = thm "CDERIV_mult";
-val NSCDERIV_cmult = thm "NSCDERIV_cmult";
-val CDERIV_cmult = thm "CDERIV_cmult";
-val NSCDERIV_minus = thm "NSCDERIV_minus";
-val CDERIV_minus = thm "CDERIV_minus";
-val NSCDERIV_add_minus = thm "NSCDERIV_add_minus";
-val CDERIV_add_minus = thm "CDERIV_add_minus";
-val NSCDERIV_diff = thm "NSCDERIV_diff";
-val CDERIV_diff = thm "CDERIV_diff";
-val NSCDERIV_zero = thm "NSCDERIV_zero";
-val NSCDERIV_capprox = thm "NSCDERIV_capprox";
-val NSCDERIVD1 = thm "NSCDERIVD1";
-val NSCDERIVD2 = thm "NSCDERIVD2";
-val lemma_complex_chain = thm "lemma_complex_chain";
-val NSCDERIV_chain = thm "NSCDERIV_chain";
-val CDERIV_chain = thm "CDERIV_chain";
-val CDERIV_chain2 = thm "CDERIV_chain2";
-val NSCDERIV_Id = thm "NSCDERIV_Id";
-val CDERIV_Id = thm "CDERIV_Id";
-val isContc_Id = thms "isContc_Id";
-val CDERIV_cmult_Id = thm "CDERIV_cmult_Id";
-val NSCDERIV_cmult_Id = thm "NSCDERIV_cmult_Id";
-val CDERIV_pow = thm "CDERIV_pow";
-val NSCDERIV_pow = thm "NSCDERIV_pow";
-val lemma_CDERIV_subst = thm "lemma_CDERIV_subst";
-val CInfinitesimal_add_not_zero = thm "CInfinitesimal_add_not_zero";
-val NSCDERIV_inverse = thm "NSCDERIV_inverse";
-val CDERIV_inverse = thm "CDERIV_inverse";
-val CDERIV_inverse_fun = thm "CDERIV_inverse_fun";
-val NSCDERIV_inverse_fun = thm "NSCDERIV_inverse_fun";
-val lemma_complex_mult_inverse_squared = thm "lemma_complex_mult_inverse_squared";
-val CDERIV_quotient = thm "CDERIV_quotient";
-val NSCDERIV_quotient = thm "NSCDERIV_quotient";
-val CLIM_equal = thm "CLIM_equal";
-val CLIM_trans = thm "CLIM_trans";
-val CARAT_CDERIV = thm "CARAT_CDERIV";
-val CARAT_NSCDERIV = thm "CARAT_NSCDERIV";
-val CARAT_CDERIVD = thm "CARAT_CDERIVD";
-*}
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Complex/CSeries.thy
--- a/src/HOL/Complex/CSeries.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Complex/CSeries.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -15,18 +15,18 @@
    sumc_Suc: "sumc m (Suc n) f = (if n < m then 0 else sumc m n f + f(n))"
 
 (*  
-constdefs
+definition
 
    needs convergence of complex sequences  
 
   csums  :: [nat=>complex,complex] => bool     (infixr 80)
-   "f sums s  == (%n. sumr 0 n f) ----C> s"
+   "f sums s  = (%n. sumr 0 n f) ----C> s"
   
    csummable :: (nat=>complex) => bool
-   "csummable f == (EX s. f csums s)"
+   "csummable f = (EX s. f csums s)"
 
    csuminf   :: (nat=>complex) => complex
-   "csuminf f == (@s. f csums s)"
+   "csuminf f = (@s. f csums s)"
 *)
 
 lemma sumc_Suc_zero [simp]: "sumc (Suc n) n f = 0"
@@ -173,34 +173,5 @@
 apply (auto simp add: sumc_split_add add_commute)
 done
 
-ML
-{*
-val sumc_Suc_zero = thm "sumc_Suc_zero";
-val sumc_eq_bounds = thm "sumc_eq_bounds";
-val sumc_Suc_eq = thm "sumc_Suc_eq";
-val sumc_add_lbound_zero = thm "sumc_add_lbound_zero";
-val sumc_add = thm "sumc_add";
-val sumc_mult = thm "sumc_mult";
-val sumc_split_add = thm "sumc_split_add";
-val sumc_split_add_minus = thm "sumc_split_add_minus";
-val sumc_cmod = thm "sumc_cmod";
-val sumc_fun_eq = thm "sumc_fun_eq";
-val sumc_const = thm "sumc_const";
-val sumc_add_mult_const = thm "sumc_add_mult_const";
-val sumc_diff_mult_const = thm "sumc_diff_mult_const";
-val sumc_less_bounds_zero = thm "sumc_less_bounds_zero";
-val sumc_minus = thm "sumc_minus";
-val sumc_shift_bounds = thm "sumc_shift_bounds";
-val sumc_minus_one_complexpow_zero = thm "sumc_minus_one_complexpow_zero";
-val sumc_interval_const = thm "sumc_interval_const";
-val sumc_interval_const2 = thm "sumc_interval_const2";
-val sumr_cmod_ge_zero = thm "sumr_cmod_ge_zero";
-val rabs_sumc_cmod_cancel = thm "rabs_sumc_cmod_cancel";
-val sumc_one_lb_complexpow_zero = thm "sumc_one_lb_complexpow_zero";
-val sumc_diff = thm "sumc_diff";
-val sumc_subst = thm "sumc_subst";
-val sumc_group = thm "sumc_group";
-*}
-
 end
 
diff -r 372065f34795 -r dfe940911617 src/HOL/Complex/CStar.thy
--- a/src/HOL/Complex/CStar.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Complex/CStar.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -36,10 +36,6 @@
     "( *f* f) (hcomplex_of_complex a) @c= hcomplex_of_complex (f a)"
 by auto
 
-(*
-Goal "( *fNat* (%n. z ^ n)) N = (hcomplex_of_complex z) hcpow N"
-*)
-
 lemma starfunC_hcpow: "( *f* (%z. z ^ n)) Z = Z hcpow hypnat_of_nat n"
 apply (cases Z)
 apply (simp add: hcpow starfun hypnat_of_nat_eq)
@@ -93,21 +89,4 @@
     "x @c= hcomplex_of_complex a ==> ( *f* (%x. x)) x @c= hcomplex_of_complex  a"
 by simp
 
-ML
-{*
-val STARC_SComplex_subset = thm "STARC_SComplex_subset";
-val STARC_hcomplex_of_complex_Int = thm "STARC_hcomplex_of_complex_Int";
-val lemma_not_hcomplexA = thm "lemma_not_hcomplexA";
-val starfun_capprox = thm "starfun_capprox";
-val starfunC_hcpow = thm "starfunC_hcpow";
-val starfun_mult_CFinite_capprox = thm "starfun_mult_CFinite_capprox";
-val starfun_add_capprox = thm "starfun_add_capprox";
-val starfunCR_cmod = thm "starfunCR_cmod";
-val starfun_inverse_inverse = thm "starfun_inverse_inverse";
-val starfun_n_diff = thm "starfun_n_diff";
-val starfunC_eq_Re_Im_iff = thm "starfunC_eq_Re_Im_iff";
-val starfunC_approx_Re_Im_iff = thm "starfunC_approx_Re_Im_iff";
-val starfunC_Idfun_capprox = thm "starfunC_Idfun_capprox";
-*}
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Complex/Complex.thy
--- a/src/HOL/Complex/Complex.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Complex/Complex.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -27,30 +27,30 @@
 lemma complex_surj [simp]: "Complex (Re z) (Im z) = z"
   by (induct z) simp
 
-constdefs
+definition
 
   (*----------- modulus ------------*)
 
   cmod :: "complex => real"
-  "cmod z == sqrt(Re(z) ^ 2 + Im(z) ^ 2)"
+  "cmod z = sqrt(Re(z) ^ 2 + Im(z) ^ 2)"
 
   (*----- injection from reals -----*)
 
   complex_of_real :: "real => complex"
-  "complex_of_real r == Complex r 0"
+  "complex_of_real r = Complex r 0"
 
   (*------- complex conjugate ------*)
 
   cnj :: "complex => complex"
-  "cnj z == Complex (Re z) (-Im z)"
+  "cnj z = Complex (Re z) (-Im z)"
 
   (*------------ Argand -------------*)
 
   sgn :: "complex => complex"
-  "sgn z == z / complex_of_real(cmod z)"
+  "sgn z = z / complex_of_real(cmod z)"
 
   arg :: "complex => real"
-  "arg z == @a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi"
+  "arg z = (SOME a. Re(sgn z) = cos a & Im(sgn z) = sin a & -pi < a & a \<le> pi)"
 
 
 defs (overloaded)
@@ -81,19 +81,19 @@
   complex_divide_def: "w / (z::complex) == w * inverse z"
 
 
-constdefs
+definition
 
   (* abbreviation for (cos a + i sin a) *)
   cis :: "real => complex"
-  "cis a == Complex (cos a) (sin a)"
+  "cis a = Complex (cos a) (sin a)"
 
   (* abbreviation for r*(cos a + i sin a) *)
   rcis :: "[real, real] => complex"
-  "rcis r a == complex_of_real r * cis a"
+  "rcis r a = complex_of_real r * cis a"
 
   (* e ^ (x + iy) *)
   expi :: "complex => complex"
-  "expi z == complex_of_real(exp (Re z)) * cis (Im z)"
+  "expi z = complex_of_real(exp (Re z)) * cis (Im z)"
 
 
 lemma complex_equality [intro?]: "Re z = Re w ==> Im z = Im w ==> z = w"
@@ -838,16 +838,16 @@
 
 
 lemma complex_of_real_of_nat [simp]: "complex_of_real (of_nat n) = of_nat n"
-by (induct n, simp_all) 
+  by (induct n) simp_all
 
 lemma complex_of_real_of_int [simp]: "complex_of_real (of_int z) = of_int z"
 proof (cases z)
   case (1 n)
-    thus ?thesis by simp
+  thus ?thesis by simp
 next
   case (2 n)
-    thus ?thesis 
-      by (simp only: of_int_minus complex_of_real_minus, simp)
+  thus ?thesis 
+    by (simp only: of_int_minus complex_of_real_minus, simp)
 qed
 
 
@@ -914,163 +914,6 @@
 test "a*(b*c)/(y*z) = d*(b::complex)*(x*a)/z";
 *)
 
-
-ML
-{*
-val complex_zero_def = thm"complex_zero_def";
-val complex_one_def = thm"complex_one_def";
-val complex_minus_def = thm"complex_minus_def";
-val complex_divide_def = thm"complex_divide_def";
-val complex_mult_def = thm"complex_mult_def";
-val complex_add_def = thm"complex_add_def";
-val complex_of_real_def = thm"complex_of_real_def";
-val i_def = thm"i_def";
-val expi_def = thm"expi_def";
-val cis_def = thm"cis_def";
-val rcis_def = thm"rcis_def";
-val cmod_def = thm"cmod_def";
-val cnj_def = thm"cnj_def";
-val sgn_def = thm"sgn_def";
-val arg_def = thm"arg_def";
-val complexpow_0 = thm"complexpow_0";
-val complexpow_Suc = thm"complexpow_Suc";
-
-val Re = thm"Re";
-val Im = thm"Im";
-val complex_Re_Im_cancel_iff = thm"complex_Re_Im_cancel_iff";
-val complex_Re_zero = thm"complex_Re_zero";
-val complex_Im_zero = thm"complex_Im_zero";
-val complex_Re_one = thm"complex_Re_one";
-val complex_Im_one = thm"complex_Im_one";
-val complex_Re_i = thm"complex_Re_i";
-val complex_Im_i = thm"complex_Im_i";
-val Re_complex_of_real = thm"Re_complex_of_real";
-val Im_complex_of_real = thm"Im_complex_of_real";
-val complex_minus = thm"complex_minus";
-val complex_Re_minus = thm"complex_Re_minus";
-val complex_Im_minus = thm"complex_Im_minus";
-val complex_add = thm"complex_add";
-val complex_Re_add = thm"complex_Re_add";
-val complex_Im_add = thm"complex_Im_add";
-val complex_add_commute = thm"complex_add_commute";
-val complex_add_assoc = thm"complex_add_assoc";
-val complex_add_zero_left = thm"complex_add_zero_left";
-val complex_add_zero_right = thm"complex_add_zero_right";
-val complex_diff = thm"complex_diff";
-val complex_mult = thm"complex_mult";
-val complex_mult_one_left = thm"complex_mult_one_left";
-val complex_mult_one_right = thm"complex_mult_one_right";
-val complex_inverse = thm"complex_inverse";
-val complex_of_real_one = thm"complex_of_real_one";
-val complex_of_real_zero = thm"complex_of_real_zero";
-val complex_of_real_eq_iff = thm"complex_of_real_eq_iff";
-val complex_of_real_minus = thm"complex_of_real_minus";
-val complex_of_real_inverse = thm"complex_of_real_inverse";
-val complex_of_real_add = thm"complex_of_real_add";
-val complex_of_real_diff = thm"complex_of_real_diff";
-val complex_of_real_mult = thm"complex_of_real_mult";
-val complex_of_real_divide = thm"complex_of_real_divide";
-val complex_of_real_pow = thm"complex_of_real_pow";
-val complex_mod = thm"complex_mod";
-val complex_mod_zero = thm"complex_mod_zero";
-val complex_mod_one = thm"complex_mod_one";
-val complex_mod_complex_of_real = thm"complex_mod_complex_of_real";
-val complex_of_real_abs = thm"complex_of_real_abs";
-val complex_cnj = thm"complex_cnj";
-val complex_cnj_cancel_iff = thm"complex_cnj_cancel_iff";
-val complex_cnj_cnj = thm"complex_cnj_cnj";
-val complex_cnj_complex_of_real = thm"complex_cnj_complex_of_real";
-val complex_mod_cnj = thm"complex_mod_cnj";
-val complex_cnj_minus = thm"complex_cnj_minus";
-val complex_cnj_inverse = thm"complex_cnj_inverse";
-val complex_cnj_add = thm"complex_cnj_add";
-val complex_cnj_diff = thm"complex_cnj_diff";
-val complex_cnj_mult = thm"complex_cnj_mult";
-val complex_cnj_divide = thm"complex_cnj_divide";
-val complex_cnj_one = thm"complex_cnj_one";
-val complex_cnj_pow = thm"complex_cnj_pow";
-val complex_add_cnj = thm"complex_add_cnj";
-val complex_diff_cnj = thm"complex_diff_cnj";
-val complex_cnj_zero = thm"complex_cnj_zero";
-val complex_cnj_zero_iff = thm"complex_cnj_zero_iff";
-val complex_mult_cnj = thm"complex_mult_cnj";
-val complex_mod_eq_zero_cancel = thm"complex_mod_eq_zero_cancel";
-val complex_mod_complex_of_real_of_nat = thm"complex_mod_complex_of_real_of_nat";
-val complex_mod_minus = thm"complex_mod_minus";
-val complex_mod_mult_cnj = thm"complex_mod_mult_cnj";
-val complex_mod_squared = thm"complex_mod_squared";
-val complex_mod_ge_zero = thm"complex_mod_ge_zero";
-val abs_cmod_cancel = thm"abs_cmod_cancel";
-val complex_mod_mult = thm"complex_mod_mult";
-val complex_mod_add_squared_eq = thm"complex_mod_add_squared_eq";
-val complex_Re_mult_cnj_le_cmod = thm"complex_Re_mult_cnj_le_cmod";
-val complex_Re_mult_cnj_le_cmod2 = thm"complex_Re_mult_cnj_le_cmod2";
-val real_sum_squared_expand = thm"real_sum_squared_expand";
-val complex_mod_triangle_squared = thm"complex_mod_triangle_squared";
-val complex_mod_minus_le_complex_mod = thm"complex_mod_minus_le_complex_mod";
-val complex_mod_triangle_ineq = thm"complex_mod_triangle_ineq";
-val complex_mod_triangle_ineq2 = thm"complex_mod_triangle_ineq2";
-val complex_mod_diff_commute = thm"complex_mod_diff_commute";
-val complex_mod_add_less = thm"complex_mod_add_less";
-val complex_mod_mult_less = thm"complex_mod_mult_less";
-val complex_mod_diff_ineq = thm"complex_mod_diff_ineq";
-val complex_Re_le_cmod = thm"complex_Re_le_cmod";
-val complex_mod_gt_zero = thm"complex_mod_gt_zero";
-val complex_mod_complexpow = thm"complex_mod_complexpow";
-val complex_mod_inverse = thm"complex_mod_inverse";
-val complex_mod_divide = thm"complex_mod_divide";
-val complexpow_i_squared = thm"complexpow_i_squared";
-val complex_i_not_zero = thm"complex_i_not_zero";
-val sgn_zero = thm"sgn_zero";
-val sgn_one = thm"sgn_one";
-val sgn_minus = thm"sgn_minus";
-val sgn_eq = thm"sgn_eq";
-val i_mult_eq = thm"i_mult_eq";
-val i_mult_eq2 = thm"i_mult_eq2";
-val Re_sgn = thm"Re_sgn";
-val Im_sgn = thm"Im_sgn";
-val complex_inverse_complex_split = thm"complex_inverse_complex_split";
-val cos_arg_i_mult_zero = thm"cos_arg_i_mult_zero";
-val complex_of_real_zero_iff = thm"complex_of_real_zero_iff";
-val rcis_Ex = thm"rcis_Ex";
-val Re_rcis = thm"Re_rcis";
-val Im_rcis = thm"Im_rcis";
-val complex_mod_rcis = thm"complex_mod_rcis";
-val complex_mod_sqrt_Re_mult_cnj = thm"complex_mod_sqrt_Re_mult_cnj";
-val complex_Re_cnj = thm"complex_Re_cnj";
-val complex_Im_cnj = thm"complex_Im_cnj";
-val complex_In_mult_cnj_zero = thm"complex_In_mult_cnj_zero";
-val complex_Re_mult = thm"complex_Re_mult";
-val complex_Re_mult_complex_of_real = thm"complex_Re_mult_complex_of_real";
-val complex_Im_mult_complex_of_real = thm"complex_Im_mult_complex_of_real";
-val complex_Re_mult_complex_of_real2 = thm"complex_Re_mult_complex_of_real2";
-val complex_Im_mult_complex_of_real2 = thm"complex_Im_mult_complex_of_real2";
-val cis_rcis_eq = thm"cis_rcis_eq";
-val rcis_mult = thm"rcis_mult";
-val cis_mult = thm"cis_mult";
-val cis_zero = thm"cis_zero";
-val rcis_zero_mod = thm"rcis_zero_mod";
-val rcis_zero_arg = thm"rcis_zero_arg";
-val complex_of_real_minus_one = thm"complex_of_real_minus_one";
-val complex_i_mult_minus = thm"complex_i_mult_minus";
-val cis_real_of_nat_Suc_mult = thm"cis_real_of_nat_Suc_mult";
-val DeMoivre = thm"DeMoivre";
-val DeMoivre2 = thm"DeMoivre2";
-val cis_inverse = thm"cis_inverse";
-val rcis_inverse = thm"rcis_inverse";
-val cis_divide = thm"cis_divide";
-val rcis_divide = thm"rcis_divide";
-val Re_cis = thm"Re_cis";
-val Im_cis = thm"Im_cis";
-val cos_n_Re_cis_pow_n = thm"cos_n_Re_cis_pow_n";
-val sin_n_Im_cis_pow_n = thm"sin_n_Im_cis_pow_n";
-val expi_add = thm"expi_add";
-val expi_zero = thm"expi_zero";
-val complex_Re_mult_eq = thm"complex_Re_mult_eq";
-val complex_Im_mult_eq = thm"complex_Im_mult_eq";
-val complex_expi_Ex = thm"complex_expi_Ex";
-*}
-
 end
 
 
diff -r 372065f34795 -r dfe940911617 src/HOL/Complex/NSCA.thy
--- a/src/HOL/Complex/NSCA.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Complex/NSCA.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -9,34 +9,34 @@
 imports NSComplex
 begin
 
-constdefs
+definition
 
    CInfinitesimal  :: "hcomplex set"
-   "CInfinitesimal == {x. \<forall>r \<in> Reals. 0 < r --> hcmod x < r}"
+   "CInfinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hcmod x < r}"
 
     capprox    :: "[hcomplex,hcomplex] => bool"  (infixl "@c=" 50)  
       --{*the ``infinitely close'' relation*}
-      "x @c= y == (x - y) \<in> CInfinitesimal"     
+      "x @c= y = ((x - y) \<in> CInfinitesimal)"     
   
    (* standard complex numbers reagarded as an embedded subset of NS complex *)
    SComplex  :: "hcomplex set"
-   "SComplex == {x. \<exists>r. x = hcomplex_of_complex r}"
+   "SComplex = {x. \<exists>r. x = hcomplex_of_complex r}"
 
    CFinite :: "hcomplex set"
-   "CFinite == {x. \<exists>r \<in> Reals. hcmod x < r}"
+   "CFinite = {x. \<exists>r \<in> Reals. hcmod x < r}"
 
    CInfinite :: "hcomplex set"
-   "CInfinite == {x. \<forall>r \<in> Reals. r < hcmod x}"
+   "CInfinite = {x. \<forall>r \<in> Reals. r < hcmod x}"
 
    stc :: "hcomplex => hcomplex"
     --{* standard part map*}
-   "stc x == (@r. x \<in> CFinite & r:SComplex & r @c= x)"
+   "stc x = (SOME r. x \<in> CFinite & r:SComplex & r @c= x)"
 
    cmonad    :: "hcomplex => hcomplex set"
-   "cmonad x  == {y. x @c= y}"
+   "cmonad x = {y. x @c= y}"
 
    cgalaxy   :: "hcomplex => hcomplex set"
-   "cgalaxy x == {y. (x - y) \<in> CFinite}"
+   "cgalaxy x = {y. (x - y) \<in> CFinite}"
 
 
 
@@ -1217,222 +1217,4 @@
      "(0 @c= hcomplex_of_complex z) = (z = 0)"
 by (simp add: star_of_zero [symmetric] del: star_of_zero)
 
-
-ML
-{*
-val SComplex_add = thm "SComplex_add";
-val SComplex_mult = thm "SComplex_mult";
-val SComplex_inverse = thm "SComplex_inverse";
-val SComplex_divide = thm "SComplex_divide";
-val SComplex_minus = thm "SComplex_minus";
-val SComplex_minus_iff = thm "SComplex_minus_iff";
-val SComplex_diff = thm "SComplex_diff";
-val SComplex_add_cancel = thm "SComplex_add_cancel";
-val SReal_hcmod_hcomplex_of_complex = thm "SReal_hcmod_hcomplex_of_complex";
-val SReal_hcmod_number_of = thm "SReal_hcmod_number_of";
-val SReal_hcmod_SComplex = thm "SReal_hcmod_SComplex";
-val SComplex_hcomplex_of_complex = thm "SComplex_hcomplex_of_complex";
-val SComplex_number_of = thm "SComplex_number_of";
-val SComplex_divide_number_of = thm "SComplex_divide_number_of";
-val SComplex_UNIV_complex = thm "SComplex_UNIV_complex";
-val SComplex_iff = thm "SComplex_iff";
-val hcomplex_of_complex_image = thm "hcomplex_of_complex_image";
-val inv_hcomplex_of_complex_image = thm "inv_hcomplex_of_complex_image";
-val SComplex_hcomplex_of_complex_image = thm "SComplex_hcomplex_of_complex_image";
-val SComplex_SReal_dense = thm "SComplex_SReal_dense";
-val SComplex_hcmod_SReal = thm "SComplex_hcmod_SReal";
-val SComplex_zero = thm "SComplex_zero";
-val SComplex_one = thm "SComplex_one";
-val CFinite_add = thm "CFinite_add";
-val CFinite_mult = thm "CFinite_mult";
-val CFinite_minus_iff = thm "CFinite_minus_iff";
-val SComplex_subset_CFinite = thm "SComplex_subset_CFinite";
-val HFinite_hcmod_hcomplex_of_complex = thm "HFinite_hcmod_hcomplex_of_complex";
-val CFinite_hcomplex_of_complex = thm "CFinite_hcomplex_of_complex";
-val CFiniteD = thm "CFiniteD";
-val CFinite_hcmod_iff = thm "CFinite_hcmod_iff";
-val CFinite_number_of = thm "CFinite_number_of";
-val CFinite_bounded = thm "CFinite_bounded";
-val CInfinitesimal_zero = thm "CInfinitesimal_zero";
-val hcomplex_sum_of_halves = thm "hcomplex_sum_of_halves";
-val CInfinitesimal_hcmod_iff = thm "CInfinitesimal_hcmod_iff";
-val one_not_CInfinitesimal = thm "one_not_CInfinitesimal";
-val CInfinitesimal_add = thm "CInfinitesimal_add";
-val CInfinitesimal_minus_iff = thm "CInfinitesimal_minus_iff";
-val CInfinitesimal_diff = thm "CInfinitesimal_diff";
-val CInfinitesimal_mult = thm "CInfinitesimal_mult";
-val CInfinitesimal_CFinite_mult = thm "CInfinitesimal_CFinite_mult";
-val CInfinitesimal_CFinite_mult2 = thm "CInfinitesimal_CFinite_mult2";
-val CInfinite_hcmod_iff = thm "CInfinite_hcmod_iff";
-val CInfinite_inverse_CInfinitesimal = thm "CInfinite_inverse_CInfinitesimal";
-val CInfinite_mult = thm "CInfinite_mult";
-val CInfinite_minus_iff = thm "CInfinite_minus_iff";
-val CFinite_sum_squares = thm "CFinite_sum_squares";
-val not_CInfinitesimal_not_zero = thm "not_CInfinitesimal_not_zero";
-val not_CInfinitesimal_not_zero2 = thm "not_CInfinitesimal_not_zero2";
-val CFinite_diff_CInfinitesimal_hcmod = thm "CFinite_diff_CInfinitesimal_hcmod";
-val hcmod_less_CInfinitesimal = thm "hcmod_less_CInfinitesimal";
-val hcmod_le_CInfinitesimal = thm "hcmod_le_CInfinitesimal";
-val CInfinitesimal_interval = thm "CInfinitesimal_interval";
-val CInfinitesimal_interval2 = thm "CInfinitesimal_interval2";
-val not_CInfinitesimal_mult = thm "not_CInfinitesimal_mult";
-val CInfinitesimal_mult_disj = thm "CInfinitesimal_mult_disj";
-val CFinite_CInfinitesimal_diff_mult = thm "CFinite_CInfinitesimal_diff_mult";
-val CInfinitesimal_subset_CFinite = thm "CInfinitesimal_subset_CFinite";
-val CInfinitesimal_hcomplex_of_complex_mult = thm "CInfinitesimal_hcomplex_of_complex_mult";
-val CInfinitesimal_hcomplex_of_complex_mult2 = thm "CInfinitesimal_hcomplex_of_complex_mult2";
-val mem_cinfmal_iff = thm "mem_cinfmal_iff";
-val capprox_minus_iff = thm "capprox_minus_iff";
-val capprox_minus_iff2 = thm "capprox_minus_iff2";
-val capprox_refl = thm "capprox_refl";
-val capprox_sym = thm "capprox_sym";
-val capprox_trans = thm "capprox_trans";
-val capprox_trans2 = thm "capprox_trans2";
-val capprox_trans3 = thm "capprox_trans3";
-val number_of_capprox_reorient = thm "number_of_capprox_reorient";
-val CInfinitesimal_capprox_minus = thm "CInfinitesimal_capprox_minus";
-val capprox_monad_iff = thm "capprox_monad_iff";
-val Infinitesimal_capprox = thm "Infinitesimal_capprox";
-val capprox_add = thm "capprox_add";
-val capprox_minus = thm "capprox_minus";
-val capprox_minus2 = thm "capprox_minus2";
-val capprox_minus_cancel = thm "capprox_minus_cancel";
-val capprox_add_minus = thm "capprox_add_minus";
-val capprox_mult1 = thm "capprox_mult1";
-val capprox_mult2 = thm "capprox_mult2";
-val capprox_mult_subst = thm "capprox_mult_subst";
-val capprox_mult_subst2 = thm "capprox_mult_subst2";
-val capprox_mult_subst_SComplex = thm "capprox_mult_subst_SComplex";
-val capprox_eq_imp = thm "capprox_eq_imp";
-val CInfinitesimal_minus_capprox = thm "CInfinitesimal_minus_capprox";
-val bex_CInfinitesimal_iff = thm "bex_CInfinitesimal_iff";
-val bex_CInfinitesimal_iff2 = thm "bex_CInfinitesimal_iff2";
-val CInfinitesimal_add_capprox = thm "CInfinitesimal_add_capprox";
-val CInfinitesimal_add_capprox_self = thm "CInfinitesimal_add_capprox_self";
-val CInfinitesimal_add_capprox_self2 = thm "CInfinitesimal_add_capprox_self2";
-val CInfinitesimal_add_minus_capprox_self = thm "CInfinitesimal_add_minus_capprox_self";
-val CInfinitesimal_add_cancel = thm "CInfinitesimal_add_cancel";
-val CInfinitesimal_add_right_cancel = thm "CInfinitesimal_add_right_cancel";
-val capprox_add_left_cancel = thm "capprox_add_left_cancel";
-val capprox_add_right_cancel = thm "capprox_add_right_cancel";
-val capprox_add_mono1 = thm "capprox_add_mono1";
-val capprox_add_mono2 = thm "capprox_add_mono2";
-val capprox_add_left_iff = thm "capprox_add_left_iff";
-val capprox_add_right_iff = thm "capprox_add_right_iff";
-val capprox_CFinite = thm "capprox_CFinite";
-val capprox_hcomplex_of_complex_CFinite = thm "capprox_hcomplex_of_complex_CFinite";
-val capprox_mult_CFinite = thm "capprox_mult_CFinite";
-val capprox_mult_hcomplex_of_complex = thm "capprox_mult_hcomplex_of_complex";
-val capprox_SComplex_mult_cancel_zero = thm "capprox_SComplex_mult_cancel_zero";
-val capprox_mult_SComplex1 = thm "capprox_mult_SComplex1";
-val capprox_mult_SComplex2 = thm "capprox_mult_SComplex2";
-val capprox_mult_SComplex_zero_cancel_iff = thm "capprox_mult_SComplex_zero_cancel_iff";
-val capprox_SComplex_mult_cancel = thm "capprox_SComplex_mult_cancel";
-val capprox_SComplex_mult_cancel_iff1 = thm "capprox_SComplex_mult_cancel_iff1";
-val capprox_hcmod_approx_zero = thm "capprox_hcmod_approx_zero";
-val capprox_approx_zero_iff = thm "capprox_approx_zero_iff";
-val capprox_minus_zero_cancel_iff = thm "capprox_minus_zero_cancel_iff";
-val Infinitesimal_hcmod_add_diff = thm "Infinitesimal_hcmod_add_diff";
-val approx_hcmod_add_hcmod = thm "approx_hcmod_add_hcmod";
-val capprox_hcmod_approx = thm "capprox_hcmod_approx";
-val CInfinitesimal_less_SComplex = thm "CInfinitesimal_less_SComplex";
-val SComplex_Int_CInfinitesimal_zero = thm "SComplex_Int_CInfinitesimal_zero";
-val SComplex_CInfinitesimal_zero = thm "SComplex_CInfinitesimal_zero";
-val SComplex_CFinite_diff_CInfinitesimal = thm "SComplex_CFinite_diff_CInfinitesimal";
-val hcomplex_of_complex_CFinite_diff_CInfinitesimal = thm "hcomplex_of_complex_CFinite_diff_CInfinitesimal";
-val hcomplex_of_complex_CInfinitesimal_iff_0 = thm "hcomplex_of_complex_CInfinitesimal_iff_0";
-val number_of_not_CInfinitesimal = thm "number_of_not_CInfinitesimal";
-val capprox_SComplex_not_zero = thm "capprox_SComplex_not_zero";
-val CFinite_diff_CInfinitesimal_capprox = thm "CFinite_diff_CInfinitesimal_capprox";
-val CInfinitesimal_ratio = thm "CInfinitesimal_ratio";
-val SComplex_capprox_iff = thm "SComplex_capprox_iff";
-val number_of_capprox_iff = thm "number_of_capprox_iff";
-val number_of_CInfinitesimal_iff = thm "number_of_CInfinitesimal_iff";
-val hcomplex_of_complex_approx_iff = thm "hcomplex_of_complex_approx_iff";
-val hcomplex_of_complex_capprox_number_of_iff = thm "hcomplex_of_complex_capprox_number_of_iff";
-val capprox_unique_complex = thm "capprox_unique_complex";
-val hcomplex_capproxD1 = thm "hcomplex_capproxD1";
-val hcomplex_capproxD2 = thm "hcomplex_capproxD2";
-val hcomplex_capproxI = thm "hcomplex_capproxI";
-val capprox_approx_iff = thm "capprox_approx_iff";
-val hcomplex_of_hypreal_capprox_iff = thm "hcomplex_of_hypreal_capprox_iff";
-val CFinite_HFinite_Re = thm "CFinite_HFinite_Re";
-val CFinite_HFinite_Im = thm "CFinite_HFinite_Im";
-val HFinite_Re_Im_CFinite = thm "HFinite_Re_Im_CFinite";
-val CFinite_HFinite_iff = thm "CFinite_HFinite_iff";
-val SComplex_Re_SReal = thm "SComplex_Re_SReal";
-val SComplex_Im_SReal = thm "SComplex_Im_SReal";
-val Reals_Re_Im_SComplex = thm "Reals_Re_Im_SComplex";
-val SComplex_SReal_iff = thm "SComplex_SReal_iff";
-val CInfinitesimal_Infinitesimal_iff = thm "CInfinitesimal_Infinitesimal_iff";
-val eq_Abs_star_Bex = thm "eq_Abs_star_Bex";
-val stc_part_Ex = thm "stc_part_Ex";
-val stc_part_Ex1 = thm "stc_part_Ex1";
-val CFinite_Int_CInfinite_empty = thm "CFinite_Int_CInfinite_empty";
-val CFinite_not_CInfinite = thm "CFinite_not_CInfinite";
-val not_CFinite_CInfinite = thm "not_CFinite_CInfinite";
-val CInfinite_CFinite_disj = thm "CInfinite_CFinite_disj";
-val CInfinite_CFinite_iff = thm "CInfinite_CFinite_iff";
-val CFinite_CInfinite_iff = thm "CFinite_CInfinite_iff";
-val CInfinite_diff_CFinite_CInfinitesimal_disj = thm "CInfinite_diff_CFinite_CInfinitesimal_disj";
-val CFinite_inverse = thm "CFinite_inverse";
-val CFinite_inverse2 = thm "CFinite_inverse2";
-val CInfinitesimal_inverse_CFinite = thm "CInfinitesimal_inverse_CFinite";
-val CFinite_not_CInfinitesimal_inverse = thm "CFinite_not_CInfinitesimal_inverse";
-val capprox_inverse = thm "capprox_inverse";
-val hcomplex_of_complex_capprox_inverse = thms "hcomplex_of_complex_capprox_inverse";
-val inverse_add_CInfinitesimal_capprox = thm "inverse_add_CInfinitesimal_capprox";
-val inverse_add_CInfinitesimal_capprox2 = thm "inverse_add_CInfinitesimal_capprox2";
-val inverse_add_CInfinitesimal_approx_CInfinitesimal = thm "inverse_add_CInfinitesimal_approx_CInfinitesimal";
-val CInfinitesimal_square_iff = thm "CInfinitesimal_square_iff";
-val capprox_CFinite_mult_cancel = thm "capprox_CFinite_mult_cancel";
-val capprox_CFinite_mult_cancel_iff1 = thm "capprox_CFinite_mult_cancel_iff1";
-val capprox_cmonad_iff = thm "capprox_cmonad_iff";
-val CInfinitesimal_cmonad_eq = thm "CInfinitesimal_cmonad_eq";
-val mem_cmonad_iff = thm "mem_cmonad_iff";
-val CInfinitesimal_cmonad_zero_iff = thm "CInfinitesimal_cmonad_zero_iff";
-val cmonad_zero_minus_iff = thm "cmonad_zero_minus_iff";
-val cmonad_zero_hcmod_iff = thm "cmonad_zero_hcmod_iff";
-val mem_cmonad_self = thm "mem_cmonad_self";
-val stc_capprox_self = thm "stc_capprox_self";
-val stc_SComplex = thm "stc_SComplex";
-val stc_CFinite = thm "stc_CFinite";
-val stc_SComplex_eq = thm "stc_SComplex_eq";
-val stc_hcomplex_of_complex = thm "stc_hcomplex_of_complex";
-val stc_eq_capprox = thm "stc_eq_capprox";
-val capprox_stc_eq = thm "capprox_stc_eq";
-val stc_eq_capprox_iff = thm "stc_eq_capprox_iff";
-val stc_CInfinitesimal_add_SComplex = thm "stc_CInfinitesimal_add_SComplex";
-val stc_CInfinitesimal_add_SComplex2 = thm "stc_CInfinitesimal_add_SComplex2";
-val CFinite_stc_CInfinitesimal_add = thm "CFinite_stc_CInfinitesimal_add";
-val stc_add = thm "stc_add";
-val stc_number_of = thm "stc_number_of";
-val stc_zero = thm "stc_zero";
-val stc_one = thm "stc_one";
-val stc_minus = thm "stc_minus";
-val stc_diff = thm "stc_diff";
-val lemma_stc_mult = thm "lemma_stc_mult";
-val stc_mult = thm "stc_mult";
-val stc_CInfinitesimal = thm "stc_CInfinitesimal";
-val stc_not_CInfinitesimal = thm "stc_not_CInfinitesimal";
-val stc_inverse = thm "stc_inverse";
-val stc_divide = thm "stc_divide";
-val stc_idempotent = thm "stc_idempotent";
-val CFinite_HFinite_hcomplex_of_hypreal = thm "CFinite_HFinite_hcomplex_of_hypreal";
-val SComplex_SReal_hcomplex_of_hypreal = thm "SComplex_SReal_hcomplex_of_hypreal";
-val stc_hcomplex_of_hypreal = thm "stc_hcomplex_of_hypreal";
-val CInfinitesimal_hcnj_iff = thm "CInfinitesimal_hcnj_iff";
-val CInfinite_HInfinite_iff = thm "CInfinite_HInfinite_iff";
-val hcomplex_split_CInfinitesimal_iff = thm "hcomplex_split_CInfinitesimal_iff";
-val hcomplex_split_CFinite_iff = thm "hcomplex_split_CFinite_iff";
-val hcomplex_split_SComplex_iff = thm "hcomplex_split_SComplex_iff";
-val hcomplex_split_CInfinite_iff = thm "hcomplex_split_CInfinite_iff";
-val hcomplex_split_capprox_iff = thm "hcomplex_split_capprox_iff";
-val complex_seq_to_hcomplex_CInfinitesimal = thm "complex_seq_to_hcomplex_CInfinitesimal";
-val CInfinitesimal_hcomplex_of_hypreal_epsilon = thm "CInfinitesimal_hcomplex_of_hypreal_epsilon";
-val hcomplex_of_complex_approx_zero_iff = thm "hcomplex_of_complex_approx_zero_iff";
-val hcomplex_of_complex_approx_zero_iff2 = thm "hcomplex_of_complex_approx_zero_iff2";
-*}
-
- 
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Complex/NSComplex.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -13,66 +13,67 @@
 
 types hcomplex = "complex star"
 
-syntax hcomplex_of_complex :: "real => real star"
-translations "hcomplex_of_complex" => "star_of :: complex => complex star"
+abbreviation
+  hcomplex_of_complex :: "complex => complex star"
+  "hcomplex_of_complex == star_of"
 
-constdefs
+definition
 
   (*--- real and Imaginary parts ---*)
 
   hRe :: "hcomplex => hypreal"
-  "hRe == *f* Re"
+  "hRe = *f* Re"
 
   hIm :: "hcomplex => hypreal"
-  "hIm == *f* Im"
+  "hIm = *f* Im"
 
 
   (*----------- modulus ------------*)
 
   hcmod :: "hcomplex => hypreal"
-  "hcmod == *f* cmod"
+  "hcmod = *f* cmod"
 
   (*------ imaginary unit ----------*)
 
   iii :: hcomplex
-  "iii == star_of ii"
+  "iii = star_of ii"
 
   (*------- complex conjugate ------*)
 
   hcnj :: "hcomplex => hcomplex"
-  "hcnj == *f* cnj"
+  "hcnj = *f* cnj"
 
   (*------------ Argand -------------*)
 
   hsgn :: "hcomplex => hcomplex"
-  "hsgn == *f* sgn"
+  "hsgn = *f* sgn"
 
   harg :: "hcomplex => hypreal"
-  "harg == *f* arg"
+  "harg = *f* arg"
 
   (* abbreviation for (cos a + i sin a) *)
   hcis :: "hypreal => hcomplex"
-  "hcis == *f* cis"
+  "hcis = *f* cis"
 
   (*----- injection from hyperreals -----*)
 
   hcomplex_of_hypreal :: "hypreal => hcomplex"
-  "hcomplex_of_hypreal == *f* complex_of_real"
+  "hcomplex_of_hypreal = *f* complex_of_real"
 
   (* abbreviation for r*(cos a + i sin a) *)
   hrcis :: "[hypreal, hypreal] => hcomplex"
-  "hrcis == *f2* rcis"
+  "hrcis = *f2* rcis"
 
   (*------------ e ^ (x + iy) ------------*)
 
   hexpi :: "hcomplex => hcomplex"
-  "hexpi == *f* expi"
+  "hexpi = *f* expi"
 
   HComplex :: "[hypreal,hypreal] => hcomplex"
-  "HComplex == *f2* Complex"
+  "HComplex = *f2* Complex"
 
   hcpow :: "[hcomplex,hypnat] => hcomplex"  (infixr "hcpow" 80)
-  "(z::hcomplex) hcpow (n::hypnat) == ( *f2* op ^) z n"
+  "(z::hcomplex) hcpow (n::hypnat) = ( *f2* op ^) z n"
 
 lemmas hcomplex_defs [transfer_unfold] =
   hRe_def hIm_def hcmod_def iii_def hcnj_def hsgn_def harg_def hcis_def
@@ -921,158 +922,4 @@
       "hIm(number_of v :: hcomplex) = 0"
 by (transfer, simp)
 
-
-ML
-{*
-val iii_def = thm"iii_def";
-
-val hRe = thm"hRe";
-val hIm = thm"hIm";
-val hcomplex_hRe_hIm_cancel_iff = thm"hcomplex_hRe_hIm_cancel_iff";
-val hcomplex_hRe_zero = thm"hcomplex_hRe_zero";
-val hcomplex_hIm_zero = thm"hcomplex_hIm_zero";
-val hcomplex_hRe_one = thm"hcomplex_hRe_one";
-val hcomplex_hIm_one = thm"hcomplex_hIm_one";
-val inj_hcomplex_of_complex = thm"inj_hcomplex_of_complex";
-val hcomplex_of_complex_i = thm"hcomplex_of_complex_i";
-val star_n_add = thm"star_n_add";
-val hRe_add = thm"hRe_add";
-val hIm_add = thm"hIm_add";
-val hRe_minus = thm"hRe_minus";
-val hIm_minus = thm"hIm_minus";
-val hcomplex_add_minus_eq_minus = thm"hcomplex_add_minus_eq_minus";
-val hcomplex_diff_eq_eq = thm"hcomplex_diff_eq_eq";
-val hcomplex_mult_minus_one = thm"hcomplex_mult_minus_one";
-val hcomplex_mult_minus_one_right = thm"hcomplex_mult_minus_one_right";
-val hcomplex_mult_left_cancel = thm"hcomplex_mult_left_cancel";
-val hcomplex_mult_right_cancel = thm"hcomplex_mult_right_cancel";
-val hcomplex_add_divide_distrib = thm"hcomplex_add_divide_distrib";
-val hcomplex_of_hypreal = thm"hcomplex_of_hypreal";
-val hcomplex_of_hypreal_cancel_iff = thm"hcomplex_of_hypreal_cancel_iff";
-val hcomplex_of_hypreal_minus = thm"hcomplex_of_hypreal_minus";
-val hcomplex_of_hypreal_inverse = thm"hcomplex_of_hypreal_inverse";
-val hcomplex_of_hypreal_add = thm"hcomplex_of_hypreal_add";
-val hcomplex_of_hypreal_diff = thm"hcomplex_of_hypreal_diff";
-val hcomplex_of_hypreal_mult = thm"hcomplex_of_hypreal_mult";
-val hcomplex_of_hypreal_divide = thm"hcomplex_of_hypreal_divide";
-val hcomplex_of_hypreal_one = thm"hcomplex_of_hypreal_one";
-val hcomplex_of_hypreal_zero = thm"hcomplex_of_hypreal_zero";
-val hcomplex_of_hypreal_pow = thm"hcomplex_of_hypreal_pow";
-val hRe_hcomplex_of_hypreal = thm"hRe_hcomplex_of_hypreal";
-val hIm_hcomplex_of_hypreal = thm"hIm_hcomplex_of_hypreal";
-val hcomplex_of_hypreal_epsilon_not_zero = thm"hcomplex_of_hypreal_epsilon_not_zero";
-val hcmod = thm"hcmod";
-val hcmod_zero = thm"hcmod_zero";
-val hcmod_one = thm"hcmod_one";
-val hcmod_hcomplex_of_hypreal = thm"hcmod_hcomplex_of_hypreal";
-val hcomplex_of_hypreal_abs = thm"hcomplex_of_hypreal_abs";
-val hcnj = thm"hcnj";
-val hcomplex_hcnj_cancel_iff = thm"hcomplex_hcnj_cancel_iff";
-val hcomplex_hcnj_hcnj = thm"hcomplex_hcnj_hcnj";
-val hcomplex_hcnj_hcomplex_of_hypreal = thm"hcomplex_hcnj_hcomplex_of_hypreal";
-val hcomplex_hmod_hcnj = thm"hcomplex_hmod_hcnj";
-val hcomplex_hcnj_minus = thm"hcomplex_hcnj_minus";
-val hcomplex_hcnj_inverse = thm"hcomplex_hcnj_inverse";
-val hcomplex_hcnj_add = thm"hcomplex_hcnj_add";
-val hcomplex_hcnj_diff = thm"hcomplex_hcnj_diff";
-val hcomplex_hcnj_mult = thm"hcomplex_hcnj_mult";
-val hcomplex_hcnj_divide = thm"hcomplex_hcnj_divide";
-val hcnj_one = thm"hcnj_one";
-val hcomplex_hcnj_pow = thm"hcomplex_hcnj_pow";
-val hcomplex_hcnj_zero = thm"hcomplex_hcnj_zero";
-val hcomplex_hcnj_zero_iff = thm"hcomplex_hcnj_zero_iff";
-val hcomplex_mult_hcnj = thm"hcomplex_mult_hcnj";
-val hcomplex_hcmod_eq_zero_cancel = thm"hcomplex_hcmod_eq_zero_cancel";
-
-val hcmod_hcomplex_of_hypreal_of_nat = thm"hcmod_hcomplex_of_hypreal_of_nat";
-val hcmod_hcomplex_of_hypreal_of_hypnat = thm"hcmod_hcomplex_of_hypreal_of_hypnat";
-val hcmod_minus = thm"hcmod_minus";
-val hcmod_mult_hcnj = thm"hcmod_mult_hcnj";
-val hcmod_ge_zero = thm"hcmod_ge_zero";
-val hrabs_hcmod_cancel = thm"hrabs_hcmod_cancel";
-val hcmod_mult = thm"hcmod_mult";
-val hcmod_add_squared_eq = thm"hcmod_add_squared_eq";
-val hcomplex_hRe_mult_hcnj_le_hcmod = thm"hcomplex_hRe_mult_hcnj_le_hcmod";
-val hcomplex_hRe_mult_hcnj_le_hcmod2 = thm"hcomplex_hRe_mult_hcnj_le_hcmod2";
-val hcmod_triangle_squared = thm"hcmod_triangle_squared";
-val hcmod_triangle_ineq = thm"hcmod_triangle_ineq";
-val hcmod_triangle_ineq2 = thm"hcmod_triangle_ineq2";
-val hcmod_diff_commute = thm"hcmod_diff_commute";
-val hcmod_add_less = thm"hcmod_add_less";
-val hcmod_mult_less = thm"hcmod_mult_less";
-val hcmod_diff_ineq = thm"hcmod_diff_ineq";
-val hcpow = thm"hcpow";
-val hcomplex_of_hypreal_hyperpow = thm"hcomplex_of_hypreal_hyperpow";
-val hcmod_hcomplexpow = thm"hcmod_hcomplexpow";
-val hcmod_hcpow = thm"hcmod_hcpow";
-val hcpow_minus = thm"hcpow_minus";
-val hcmod_hcomplex_inverse = thm"hcmod_hcomplex_inverse";
-val hcmod_divide = thm"hcmod_divide";
-val hcpow_mult = thm"hcpow_mult";
-val hcpow_zero = thm"hcpow_zero";
-val hcpow_zero2 = thm"hcpow_zero2";
-val hcpow_not_zero = thm"hcpow_not_zero";
-val hcpow_zero_zero = thm"hcpow_zero_zero";
-val hcomplex_i_mult_eq = thm"hcomplex_i_mult_eq";
-val hcomplexpow_i_squared = thm"hcomplexpow_i_squared";
-val hcomplex_i_not_zero = thm"hcomplex_i_not_zero";
-val star_n_divide = thm"star_n_divide";
-val hsgn = thm"hsgn";
-val hsgn_zero = thm"hsgn_zero";
-val hsgn_one = thm"hsgn_one";
-val hsgn_minus = thm"hsgn_minus";
-val hsgn_eq = thm"hsgn_eq";
-val lemma_hypreal_P_EX2 = thm"lemma_hypreal_P_EX2";
-val hcmod_i = thm"hcmod_i";
-val hcomplex_eq_cancel_iff2 = thm"hcomplex_eq_cancel_iff2";
-val hRe_hsgn = thm"hRe_hsgn";
-val hIm_hsgn = thm"hIm_hsgn";
-val real_two_squares_add_zero_iff = thm"real_two_squares_add_zero_iff";
-val hRe_mult_i_eq = thm"hRe_mult_i_eq";
-val hIm_mult_i_eq = thm"hIm_mult_i_eq";
-val hcmod_mult_i = thm"hcmod_mult_i";
-val hcmod_mult_i2 = thm"hcmod_mult_i2";
-val harg = thm"harg";
-val cos_harg_i_mult_zero = thm"cos_harg_i_mult_zero";
-val hcomplex_of_hypreal_zero_iff = thm"hcomplex_of_hypreal_zero_iff";
-val complex_split_polar2 = thm"complex_split_polar2";
-val hcomplex_split_polar = thm"hcomplex_split_polar";
-val hcis = thm"hcis";
-val hcis_eq = thm"hcis_eq";
-val hrcis = thm"hrcis";
-val hrcis_Ex = thm"hrcis_Ex";
-val hRe_hcomplex_polar = thm"hRe_hcomplex_polar";
-val hRe_hrcis = thm"hRe_hrcis";
-val hIm_hcomplex_polar = thm"hIm_hcomplex_polar";
-val hIm_hrcis = thm"hIm_hrcis";
-val hcmod_complex_polar = thm"hcmod_complex_polar";
-val hcmod_hrcis = thm"hcmod_hrcis";
-val hcis_hrcis_eq = thm"hcis_hrcis_eq";
-val hrcis_mult = thm"hrcis_mult";
-val hcis_mult = thm"hcis_mult";
-val hcis_zero = thm"hcis_zero";
-val hrcis_zero_mod = thm"hrcis_zero_mod";
-val hrcis_zero_arg = thm"hrcis_zero_arg";
-val hcomplex_i_mult_minus = thm"hcomplex_i_mult_minus";
-val hcomplex_i_mult_minus2 = thm"hcomplex_i_mult_minus2";
-val hcis_hypreal_of_nat_Suc_mult = thm"hcis_hypreal_of_nat_Suc_mult";
-val NSDeMoivre = thm"NSDeMoivre";
-val hcis_hypreal_of_hypnat_Suc_mult = thm"hcis_hypreal_of_hypnat_Suc_mult";
-val NSDeMoivre_ext = thm"NSDeMoivre_ext";
-val DeMoivre2 = thm"DeMoivre2";
-val DeMoivre2_ext = thm"DeMoivre2_ext";
-val hcis_inverse = thm"hcis_inverse";
-val hrcis_inverse = thm"hrcis_inverse";
-val hRe_hcis = thm"hRe_hcis";
-val hIm_hcis = thm"hIm_hcis";
-val cos_n_hRe_hcis_pow_n = thm"cos_n_hRe_hcis_pow_n";
-val sin_n_hIm_hcis_pow_n = thm"sin_n_hIm_hcis_pow_n";
-val cos_n_hRe_hcis_hcpow_n = thm"cos_n_hRe_hcis_hcpow_n";
-val sin_n_hIm_hcis_hcpow_n = thm"sin_n_hIm_hcis_hcpow_n";
-val hexpi_add = thm"hexpi_add";
-val hRe_hcomplex_of_complex = thm"hRe_hcomplex_of_complex";
-val hIm_hcomplex_of_complex = thm"hIm_hcomplex_of_complex";
-val hcmod_hcomplex_of_complex = thm"hcmod_hcomplex_of_complex";
-*}
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/EvenOdd.thy
--- a/src/HOL/Hyperreal/EvenOdd.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/EvenOdd.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -86,24 +86,4 @@
 lemma lemma_even_mod_4_div_2: "n mod 4 = (1::nat) ==> even ((n - 1) div 2)"
 by (rule_tac t = n and n1 = 4 in mod_div_equality [THEN subst], simp)
 
-ML
-{*
-val even_nat_Suc = thm"Parity.even_nat_Suc";
-
-val even_mult_two_ex = thm "even_mult_two_ex";
-val odd_Suc_mult_two_ex = thm "odd_Suc_mult_two_ex";
-val even_add = thm "even_add";
-val odd_add = thm "odd_add";
-val Suc_n_div_2_gt_zero = thm "Suc_n_div_2_gt_zero";
-val div_2_gt_zero = thm "div_2_gt_zero";
-val even_num_iff = thm "even_num_iff";
-val nat_mod_div_trivial = thm "nat_mod_div_trivial";
-val nat_mod_mod_trivial = thm "nat_mod_mod_trivial";
-val mod_Suc_eq_Suc_mod = thm "mod_Suc_eq_Suc_mod";
-val even_even_mod_4_iff = thm "even_even_mod_4_iff";
-val lemma_odd_mod_4_div_2 = thm "lemma_odd_mod_4_div_2";
-val lemma_even_mod_4_div_2 = thm "lemma_even_mod_4_div_2";
-*}
-
 end
-
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/Fact.thy
--- a/src/HOL/Hyperreal/Fact.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/Fact.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -12,65 +12,65 @@
 
 consts fact :: "nat => nat"
 primrec
-   fact_0:     "fact 0 = 1"
-   fact_Suc:   "fact (Suc n) = (Suc n) * fact n"
+  fact_0:     "fact 0 = 1"
+  fact_Suc:   "fact (Suc n) = (Suc n) * fact n"
 
 
 lemma fact_gt_zero [simp]: "0 < fact n"
-by (induct "n", auto)
+  by (induct n) auto
 
 lemma fact_not_eq_zero [simp]: "fact n \<noteq> 0"
-by simp
+  by simp
 
 lemma real_of_nat_fact_not_zero [simp]: "real (fact n) \<noteq> 0"
-by auto
+  by auto
 
 lemma real_of_nat_fact_gt_zero [simp]: "0 < real(fact n)"
-by auto
+  by auto
 
 lemma real_of_nat_fact_ge_zero [simp]: "0 \<le> real(fact n)"
-by simp
+  by simp
 
 lemma fact_ge_one [simp]: "1 \<le> fact n"
-by (induct "n", auto)
+  by (induct n) auto
 
 lemma fact_mono: "m \<le> n ==> fact m \<le> fact n"
-apply (drule le_imp_less_or_eq)
-apply (auto dest!: less_imp_Suc_add)
-apply (induct_tac "k", auto)
-done
+  apply (drule le_imp_less_or_eq)
+  apply (auto dest!: less_imp_Suc_add)
+  apply (induct_tac k, auto)
+  done
 
 text{*Note that @{term "fact 0 = fact 1"}*}
 lemma fact_less_mono: "[| 0 < m; m < n |] ==> fact m < fact n"
-apply (drule_tac m = m in less_imp_Suc_add, auto)
-apply (induct_tac "k", auto)
-done
+  apply (drule_tac m = m in less_imp_Suc_add, auto)
+  apply (induct_tac k, auto)
+  done
 
 lemma inv_real_of_nat_fact_gt_zero [simp]: "0 < inverse (real (fact n))"
-by (auto simp add: positive_imp_inverse_positive)
+  by (auto simp add: positive_imp_inverse_positive)
 
 lemma inv_real_of_nat_fact_ge_zero [simp]: "0 \<le> inverse (real (fact n))"
-by (auto intro: order_less_imp_le)
+  by (auto intro: order_less_imp_le)
 
 lemma fact_diff_Suc [rule_format]:
-     "\<forall>m. n < Suc m --> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
-apply (induct n, auto)
-apply (drule_tac x = "m - 1" in spec, auto)
-done
+    "n < Suc m ==> fact (Suc m - n) = (Suc m - n) * fact (m - n)"
+  apply (induct n fixing: m)
+  apply auto
+  apply (drule_tac x = "m - 1" in meta_spec, auto)
+  done
 
 lemma fact_num0 [simp]: "fact 0 = 1"
-by auto
+  by auto
 
 lemma fact_num_eq_if: "fact m = (if m=0 then 1 else m * fact (m - 1))"
-by (case_tac "m", auto)
+  by (cases m) auto
 
 lemma fact_add_num_eq_if:
-     "fact (m+n) = (if (m+n = 0) then 1 else (m+n) * (fact (m + n - 1)))"
-by (case_tac "m+n", auto)
+    "fact (m + n) = (if m + n = 0 then 1 else (m + n) * fact (m + n - 1))"
+  by (cases "m + n") auto
 
 lemma fact_add_num_eq_if2:
-     "fact (m+n) = (if m=0 then fact n else (m+n) * (fact ((m - 1) + n)))"
-by (case_tac "m", auto)
-
+    "fact (m + n) = (if m = 0 then fact n else (m + n) * fact ((m - 1) + n))"
+  by (cases m) auto
 
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/HLog.thy
--- a/src/HOL/Hyperreal/HLog.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/HLog.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -18,13 +18,12 @@
 by auto
 
 
-constdefs
-
-    powhr  :: "[hypreal,hypreal] => hypreal"     (infixr "powhr" 80)
-    "x powhr a == starfun2 (op powr) x a"
+definition
+  powhr  :: "[hypreal,hypreal] => hypreal"     (infixr "powhr" 80)
+  "x powhr a = starfun2 (op powr) x a"
   
-    hlog :: "[hypreal,hypreal] => hypreal"
-    "hlog a x == starfun2 log a x"
+  hlog :: "[hypreal,hypreal] => hypreal"
+  "hlog a x = starfun2 log a x"
 
 declare powhr_def [transfer_unfold]
 declare hlog_def [transfer_unfold]
@@ -156,41 +155,4 @@
      "[| 1 < a; 0 < x; 0 < y |] ==> (hlog a x \<le> hlog a y) = (x \<le> y)"
 by (simp add: linorder_not_less [symmetric])
 
-
-ML
-{*
-val powhr = thm "powhr";
-val powhr_one_eq_one = thm "powhr_one_eq_one";
-val powhr_mult = thm "powhr_mult";
-val powhr_gt_zero = thm "powhr_gt_zero";
-val powhr_not_zero = thm "powhr_not_zero";
-val powhr_divide = thm "powhr_divide";
-val powhr_add = thm "powhr_add";
-val powhr_powhr = thm "powhr_powhr";
-val powhr_powhr_swap = thm "powhr_powhr_swap";
-val powhr_minus = thm "powhr_minus";
-val powhr_minus_divide = thm "powhr_minus_divide";
-val powhr_less_mono = thm "powhr_less_mono";
-val powhr_less_cancel = thm "powhr_less_cancel";
-val powhr_less_cancel_iff = thm "powhr_less_cancel_iff";
-val powhr_le_cancel_iff = thm "powhr_le_cancel_iff";
-val hlog = thm "hlog";
-val hlog_starfun_ln = thm "hlog_starfun_ln";
-val powhr_hlog_cancel = thm "powhr_hlog_cancel";
-val hlog_powhr_cancel = thm "hlog_powhr_cancel";
-val hlog_mult = thm "hlog_mult";
-val hlog_as_starfun = thm "hlog_as_starfun";
-val hlog_eq_div_starfun_ln_mult_hlog = thm "hlog_eq_div_starfun_ln_mult_hlog";
-val powhr_as_starfun = thm "powhr_as_starfun";
-val HInfinite_powhr = thm "HInfinite_powhr";
-val hlog_hrabs_HInfinite_Infinitesimal = thm "hlog_hrabs_HInfinite_Infinitesimal";
-val hlog_HInfinite_as_starfun = thm "hlog_HInfinite_as_starfun";
-val hlog_one = thm "hlog_one";
-val hlog_eq_one = thm "hlog_eq_one";
-val hlog_inverse = thm "hlog_inverse";
-val hlog_divide = thm "hlog_divide";
-val hlog_less_cancel_iff = thm "hlog_less_cancel_iff";
-val hlog_le_cancel_iff = thm "hlog_le_cancel_iff";
-*}
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/HSeries.thy
--- a/src/HOL/Hyperreal/HSeries.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/HSeries.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -11,19 +11,19 @@
 imports Series
 begin
 
-constdefs 
+definition
   sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
-   "sumhr == 
-      %(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N"
+  "sumhr = 
+      (%(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N)"
 
   NSsums  :: "[nat=>real,real] => bool"     (infixr "NSsums" 80)
-   "f NSsums s  == (%n. setsum f {0..<n}) ----NS> s"
+  "f NSsums s = (%n. setsum f {0..<n}) ----NS> s"
 
   NSsummable :: "(nat=>real) => bool"
-   "NSsummable f == (\<exists>s. f NSsums s)"
+  "NSsummable f = (\<exists>s. f NSsums s)"
 
   NSsuminf   :: "(nat=>real) => real"
-   "NSsuminf f == (@s. f NSsums s)"
+  "NSsuminf f = (SOME s. f NSsums s)"
 
 
 lemma sumhr:
@@ -230,42 +230,4 @@
 apply (auto)
 done
 
-ML
-{*
-val sumhr = thm "sumhr";
-val sumhr_zero = thm "sumhr_zero";
-val sumhr_if = thm "sumhr_if";
-val sumhr_Suc_zero = thm "sumhr_Suc_zero";
-val sumhr_eq_bounds = thm "sumhr_eq_bounds";
-val sumhr_Suc = thm "sumhr_Suc";
-val sumhr_add_lbound_zero = thm "sumhr_add_lbound_zero";
-val sumhr_add = thm "sumhr_add";
-val sumhr_mult = thm "sumhr_mult";
-val sumhr_split_add = thm "sumhr_split_add";
-val sumhr_split_diff = thm "sumhr_split_diff";
-val sumhr_hrabs = thm "sumhr_hrabs";
-val sumhr_fun_hypnat_eq = thm "sumhr_fun_hypnat_eq";
-val sumhr_less_bounds_zero = thm "sumhr_less_bounds_zero";
-val sumhr_minus = thm "sumhr_minus";
-val sumhr_shift_bounds = thm "sumhr_shift_bounds";
-val sumhr_hypreal_of_hypnat_omega = thm "sumhr_hypreal_of_hypnat_omega";
-val sumhr_hypreal_omega_minus_one = thm "sumhr_hypreal_omega_minus_one";
-val sumhr_minus_one_realpow_zero = thm "sumhr_minus_one_realpow_zero";
-val sumhr_interval_const = thm "sumhr_interval_const";
-val starfunNat_sumr = thm "starfunNat_sumr";
-val sumhr_hrabs_approx = thm "sumhr_hrabs_approx";
-val sums_NSsums_iff = thm "sums_NSsums_iff";
-val summable_NSsummable_iff = thm "summable_NSsummable_iff";
-val suminf_NSsuminf_iff = thm "suminf_NSsuminf_iff";
-val NSsums_NSsummable = thm "NSsums_NSsummable";
-val NSsummable_NSsums = thm "NSsummable_NSsums";
-val NSsums_unique = thm "NSsums_unique";
-val NSseries_zero = thm "NSseries_zero";
-val NSsummable_NSCauchy = thm "NSsummable_NSCauchy";
-val NSsummable_NSLIMSEQ_zero = thm "NSsummable_NSLIMSEQ_zero";
-val summable_LIMSEQ_zero = thm "summable_LIMSEQ_zero";
-val NSsummable_comparison_test = thm "NSsummable_comparison_test";
-val NSsummable_rabs_comparison_test = thm "NSsummable_rabs_comparison_test";
-*}
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -30,18 +30,17 @@
 qed
 
 
-constdefs
-
+definition
   exphr :: "real => hypreal"
     --{*define exponential function using standard part *}
-    "exphr x ==  st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))" 
+  "exphr x =  st(sumhr (0, whn, %n. inverse(real (fact n)) * (x ^ n)))"
 
   sinhr :: "real => hypreal"
-    "sinhr x == st(sumhr (0, whn, %n. (if even(n) then 0 else
+  "sinhr x = st(sumhr (0, whn, %n. (if even(n) then 0 else
              ((-1) ^ ((n - 1) div 2))/(real (fact n))) * (x ^ n)))"
   
   coshr :: "real => hypreal"
-    "coshr x == st(sumhr (0, whn, %n. (if even(n) then
+  "coshr x = st(sumhr (0, whn, %n. (if even(n) then
             ((-1) ^ (n div 2))/(real (fact n)) else 0) * x ^ n))"
 
 
@@ -616,98 +615,4 @@
             simp add: Infinitesimal_approx_minus [symmetric] numeral_2_eq_2)
 done
 
-ML
-{*
-val STAR_sqrt_zero = thm "STAR_sqrt_zero";
-val STAR_sqrt_one = thm "STAR_sqrt_one";
-val hypreal_sqrt_pow2_iff = thm "hypreal_sqrt_pow2_iff";
-val hypreal_sqrt_gt_zero_pow2 = thm "hypreal_sqrt_gt_zero_pow2";
-val hypreal_sqrt_pow2_gt_zero = thm "hypreal_sqrt_pow2_gt_zero";
-val hypreal_sqrt_not_zero = thm "hypreal_sqrt_not_zero";
-val hypreal_inverse_sqrt_pow2 = thm "hypreal_inverse_sqrt_pow2";
-val hypreal_sqrt_mult_distrib = thm "hypreal_sqrt_mult_distrib";
-val hypreal_sqrt_mult_distrib2 = thm "hypreal_sqrt_mult_distrib2";
-val hypreal_sqrt_approx_zero = thm "hypreal_sqrt_approx_zero";
-val hypreal_sqrt_approx_zero2 = thm "hypreal_sqrt_approx_zero2";
-val hypreal_sqrt_sum_squares = thm "hypreal_sqrt_sum_squares";
-val hypreal_sqrt_sum_squares2 = thm "hypreal_sqrt_sum_squares2";
-val hypreal_sqrt_gt_zero = thm "hypreal_sqrt_gt_zero";
-val hypreal_sqrt_ge_zero = thm "hypreal_sqrt_ge_zero";
-val hypreal_sqrt_hrabs = thm "hypreal_sqrt_hrabs";
-val hypreal_sqrt_hrabs2 = thm "hypreal_sqrt_hrabs2";
-val hypreal_sqrt_hyperpow_hrabs = thm "hypreal_sqrt_hyperpow_hrabs";
-val star_sqrt_HFinite = thm "star_sqrt_HFinite";
-val st_hypreal_sqrt = thm "st_hypreal_sqrt";
-val hypreal_sqrt_sum_squares_ge1 = thm "hypreal_sqrt_sum_squares_ge1";
-val HFinite_hypreal_sqrt = thm "HFinite_hypreal_sqrt";
-val HFinite_hypreal_sqrt_imp_HFinite = thm "HFinite_hypreal_sqrt_imp_HFinite";
-val HFinite_hypreal_sqrt_iff = thm "HFinite_hypreal_sqrt_iff";
-val HFinite_sqrt_sum_squares = thm "HFinite_sqrt_sum_squares";
-val Infinitesimal_hypreal_sqrt = thm "Infinitesimal_hypreal_sqrt";
-val Infinitesimal_hypreal_sqrt_imp_Infinitesimal = thm "Infinitesimal_hypreal_sqrt_imp_Infinitesimal";
-val Infinitesimal_hypreal_sqrt_iff = thm "Infinitesimal_hypreal_sqrt_iff";
-val Infinitesimal_sqrt_sum_squares = thm "Infinitesimal_sqrt_sum_squares";
-val HInfinite_hypreal_sqrt = thm "HInfinite_hypreal_sqrt";
-val HInfinite_hypreal_sqrt_imp_HInfinite = thm "HInfinite_hypreal_sqrt_imp_HInfinite";
-val HInfinite_hypreal_sqrt_iff = thm "HInfinite_hypreal_sqrt_iff";
-val HInfinite_sqrt_sum_squares = thm "HInfinite_sqrt_sum_squares";
-val HFinite_exp = thm "HFinite_exp";
-val exphr_zero = thm "exphr_zero";
-val coshr_zero = thm "coshr_zero";
-val STAR_exp_zero_approx_one = thm "STAR_exp_zero_approx_one";
-val STAR_exp_Infinitesimal = thm "STAR_exp_Infinitesimal";
-val STAR_exp_epsilon = thm "STAR_exp_epsilon";
-val STAR_exp_add = thm "STAR_exp_add";
-val exphr_hypreal_of_real_exp_eq = thm "exphr_hypreal_of_real_exp_eq";
-val starfun_exp_ge_add_one_self = thm "starfun_exp_ge_add_one_self";
-val starfun_exp_HInfinite = thm "starfun_exp_HInfinite";
-val starfun_exp_minus = thm "starfun_exp_minus";
-val starfun_exp_Infinitesimal = thm "starfun_exp_Infinitesimal";
-val starfun_exp_gt_one = thm "starfun_exp_gt_one";
-val starfun_ln_exp = thm "starfun_ln_exp";
-val starfun_exp_ln_iff = thm "starfun_exp_ln_iff";
-val starfun_exp_ln_eq = thm "starfun_exp_ln_eq";
-val starfun_ln_less_self = thm "starfun_ln_less_self";
-val starfun_ln_ge_zero = thm "starfun_ln_ge_zero";
-val starfun_ln_gt_zero = thm "starfun_ln_gt_zero";
-val starfun_ln_not_eq_zero = thm "starfun_ln_not_eq_zero";
-val starfun_ln_HFinite = thm "starfun_ln_HFinite";
-val starfun_ln_inverse = thm "starfun_ln_inverse";
-val starfun_exp_HFinite = thm "starfun_exp_HFinite";
-val starfun_exp_add_HFinite_Infinitesimal_approx = thm "starfun_exp_add_HFinite_Infinitesimal_approx";
-val starfun_ln_HInfinite = thm "starfun_ln_HInfinite";
-val starfun_exp_HInfinite_Infinitesimal_disj = thm "starfun_exp_HInfinite_Infinitesimal_disj";
-val starfun_ln_HFinite_not_Infinitesimal = thm "starfun_ln_HFinite_not_Infinitesimal";
-val starfun_ln_Infinitesimal_HInfinite = thm "starfun_ln_Infinitesimal_HInfinite";
-val starfun_ln_less_zero = thm "starfun_ln_less_zero";
-val starfun_ln_Infinitesimal_less_zero = thm "starfun_ln_Infinitesimal_less_zero";
-val starfun_ln_HInfinite_gt_zero = thm "starfun_ln_HInfinite_gt_zero";
-val HFinite_sin = thm "HFinite_sin";
-val STAR_sin_zero = thm "STAR_sin_zero";
-val STAR_sin_Infinitesimal = thm "STAR_sin_Infinitesimal";
-val HFinite_cos = thm "HFinite_cos";
-val STAR_cos_zero = thm "STAR_cos_zero";
-val STAR_cos_Infinitesimal = thm "STAR_cos_Infinitesimal";
-val STAR_tan_zero = thm "STAR_tan_zero";
-val STAR_tan_Infinitesimal = thm "STAR_tan_Infinitesimal";
-val STAR_sin_cos_Infinitesimal_mult = thm "STAR_sin_cos_Infinitesimal_mult";
-val HFinite_pi = thm "HFinite_pi";
-val lemma_split_hypreal_of_real = thm "lemma_split_hypreal_of_real";
-val STAR_sin_Infinitesimal_divide = thm "STAR_sin_Infinitesimal_divide";
-val lemma_sin_pi = thm "lemma_sin_pi";
-val STAR_sin_inverse_HNatInfinite = thm "STAR_sin_inverse_HNatInfinite";
-val Infinitesimal_pi_divide_HNatInfinite = thm "Infinitesimal_pi_divide_HNatInfinite";
-val pi_divide_HNatInfinite_not_zero = thm "pi_divide_HNatInfinite_not_zero";
-val STAR_sin_pi_divide_HNatInfinite_approx_pi = thm "STAR_sin_pi_divide_HNatInfinite_approx_pi";
-val STAR_sin_pi_divide_HNatInfinite_approx_pi2 = thm "STAR_sin_pi_divide_HNatInfinite_approx_pi2";
-val starfunNat_pi_divide_n_Infinitesimal = thm "starfunNat_pi_divide_n_Infinitesimal";
-val STAR_sin_pi_divide_n_approx = thm "STAR_sin_pi_divide_n_approx";
-val NSLIMSEQ_sin_pi = thm "NSLIMSEQ_sin_pi";
-val NSLIMSEQ_cos_one = thm "NSLIMSEQ_cos_one";
-val NSLIMSEQ_sin_cos_pi = thm "NSLIMSEQ_sin_cos_pi";
-val STAR_cos_Infinitesimal_approx = thm "STAR_cos_Infinitesimal_approx";
-val STAR_cos_Infinitesimal_approx2 = thm "STAR_cos_Infinitesimal_approx2";
-*}
-
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/HyperArith.thy
--- a/src/HOL/Hyperreal/HyperArith.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/HyperArith.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -23,14 +23,12 @@
      "[| abs x < r; abs y < s |] ==> abs(x+y) < r + (s::hypreal)"
 by (simp add: abs_if split: split_if_asm)
 
-text{*used once in NSA*}
 lemma hrabs_less_gt_zero: "abs x < r ==> (0::hypreal) < r"
 by (blast intro!: order_le_less_trans abs_ge_zero)
 
 lemma hrabs_disj: "abs x = (x::hypreal) | abs x = -x"
 by (simp add: abs_if)
 
-(* Needed in Geom.ML *)
 lemma hrabs_add_lemma_disj: "(y::hypreal) + - x + (y + - z) = abs (x + - z) ==> y = z | x = y"
 by (simp add: abs_if split add: split_if_asm)
 
@@ -41,9 +39,9 @@
 
 subsection{*Embedding the Naturals into the Hyperreals*}
 
-constdefs
+definition
   hypreal_of_nat   :: "nat => hypreal"
-   "hypreal_of_nat m == of_nat m"
+  "hypreal_of_nat m = of_nat m"
 
 lemma SNat_eq: "Nats = {n. \<exists>N. n = hypreal_of_nat N}"
 by (force simp add: hypreal_of_nat_def Nats_def) 
@@ -111,24 +109,4 @@
 Addsimps [symmetric hypreal_diff_def]
 *)
 
-ML
-{*
-val hypreal_of_nat_def = thm"hypreal_of_nat_def";
-
-val hrabs_add_less = thm "hrabs_add_less";
-val hrabs_disj = thm "hrabs_disj";
-val hrabs_add_lemma_disj = thm "hrabs_add_lemma_disj";
-val hypreal_of_real_hrabs = thm "hypreal_of_real_hrabs";
-val hypreal_of_nat_add = thm "hypreal_of_nat_add";
-val hypreal_of_nat_mult = thm "hypreal_of_nat_mult";
-val hypreal_of_nat_less_iff = thm "hypreal_of_nat_less_iff";
-val hypreal_of_nat_Suc = thm "hypreal_of_nat_Suc";
-val hypreal_of_nat_number_of = thm "hypreal_of_nat_number_of";
-val hypreal_of_nat_zero = thm "hypreal_of_nat_zero";
-val hypreal_of_nat_one = thm "hypreal_of_nat_one";
-val hypreal_of_nat_le_iff = thm"hypreal_of_nat_le_iff";
-val hypreal_of_nat_ge_zero = thm"hypreal_of_nat_ge_zero";
-val hypreal_of_nat = thm"hypreal_of_nat";
-*}
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -18,21 +18,20 @@
   hypreal_of_real :: "real => real star"
   "hypreal_of_real == star_of"
 
-constdefs
-
+definition
   omega   :: hypreal   -- {*an infinite number @{text "= [<1,2,3,...>]"} *}
-  "omega == star_n (%n. real (Suc n))"
+  "omega = star_n (%n. real (Suc n))"
 
   epsilon :: hypreal   -- {*an infinitesimal number @{text "= [<1,1/2,1/3,...>]"} *}
-  "epsilon == star_n (%n. inverse (real (Suc n)))"
+  "epsilon = star_n (%n. inverse (real (Suc n)))"
 
-syntax (xsymbols)
-  omega   :: hypreal   ("\<omega>")
-  epsilon :: hypreal   ("\<epsilon>")
+const_syntax (xsymbols)
+  omega  ("\<omega>")
+  epsilon  ("\<epsilon>")
 
-syntax (HTML output)
-  omega   :: hypreal   ("\<omega>")
-  epsilon :: hypreal   ("\<epsilon>")
+const_syntax (HTML output)
+  omega  ("\<omega>")
+  epsilon  ("\<epsilon>")
 
 
 subsection{*Existence of Free Ultrafilter over the Naturals*}
@@ -302,60 +301,4 @@
 lemma hypreal_epsilon_inverse_omega: "epsilon = inverse(omega)"
 by (simp add: epsilon_def omega_def star_n_inverse)
 
-
-ML
-{*
-val omega_def = thm "omega_def";
-val epsilon_def = thm "epsilon_def";
-
-val FreeUltrafilterNat_Ex = thm "FreeUltrafilterNat_Ex";
-val FreeUltrafilterNat_mem = thm "FreeUltrafilterNat_mem";
-val FreeUltrafilterNat_finite = thm "FreeUltrafilterNat_finite";
-val FreeUltrafilterNat_not_finite = thm "FreeUltrafilterNat_not_finite";
-val FreeUltrafilterNat_empty = thm "FreeUltrafilterNat_empty";
-val FreeUltrafilterNat_Int = thm "FreeUltrafilterNat_Int";
-val FreeUltrafilterNat_subset = thm "FreeUltrafilterNat_subset";
-val FreeUltrafilterNat_Compl = thm "FreeUltrafilterNat_Compl";
-val FreeUltrafilterNat_Compl_mem = thm "FreeUltrafilterNat_Compl_mem";
-val FreeUltrafilterNat_Compl_iff1 = thm "FreeUltrafilterNat_Compl_iff1";
-val FreeUltrafilterNat_Compl_iff2 = thm "FreeUltrafilterNat_Compl_iff2";
-val FreeUltrafilterNat_UNIV = thm "FreeUltrafilterNat_UNIV";
-val FreeUltrafilterNat_Nat_set_refl = thm "FreeUltrafilterNat_Nat_set_refl";
-val FreeUltrafilterNat_P = thm "FreeUltrafilterNat_P";
-val FreeUltrafilterNat_Ex_P = thm "FreeUltrafilterNat_Ex_P";
-val FreeUltrafilterNat_all = thm "FreeUltrafilterNat_all";
-val FreeUltrafilterNat_Un = thm "FreeUltrafilterNat_Un";
-val starrel_iff = thm "starrel_iff";
-val starrel_in_hypreal = thm "starrel_in_hypreal";
-val Abs_star_inverse = thm "Abs_star_inverse";
-val lemma_starrel_refl = thm "lemma_starrel_refl";
-val hypreal_empty_not_mem = thm "hypreal_empty_not_mem";
-val Rep_hypreal_nonempty = thm "Rep_hypreal_nonempty";
-val inj_hypreal_of_real = thm "inj_hypreal_of_real";
-(* val eq_Abs_star = thm "eq_Abs_star"; *)
-val star_n_minus = thm "star_n_minus";
-val star_n_add = thm "star_n_add";
-val star_n_diff = thm "star_n_diff";
-val star_n_mult = thm "star_n_mult";
-val star_n_inverse = thm "star_n_inverse";
-val hypreal_mult_left_cancel = thm "hypreal_mult_left_cancel";
-val hypreal_mult_right_cancel = thm "hypreal_mult_right_cancel";
-val hypreal_not_refl2 = thm "hypreal_not_refl2";
-val star_n_less = thm "star_n_less";
-val hypreal_eq_minus_iff = thm "hypreal_eq_minus_iff";
-val star_n_le = thm "star_n_le";
-val star_n_zero_num = thm "star_n_zero_num";
-val star_n_one_num = thm "star_n_one_num";
-val hypreal_omega_gt_zero = thm "hypreal_omega_gt_zero";
-
-val lemma_omega_empty_singleton_disj = thm"lemma_omega_empty_singleton_disj";
-val lemma_finite_omega_set = thm"lemma_finite_omega_set";
-val not_ex_hypreal_of_real_eq_omega = thm"not_ex_hypreal_of_real_eq_omega";
-val hypreal_of_real_not_eq_omega = thm"hypreal_of_real_not_eq_omega";
-val not_ex_hypreal_of_real_eq_epsilon = thm"not_ex_hypreal_of_real_eq_epsilon";
-val hypreal_of_real_not_eq_epsilon = thm"hypreal_of_real_not_eq_epsilon";
-val hypreal_epsilon_not_zero = thm"hypreal_epsilon_not_zero";
-val hypreal_epsilon_inverse_omega = thm"hypreal_epsilon_inverse_omega";
-*}
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -148,11 +148,10 @@
 
 subsection{*Existence of an infinite hypernatural number*}
 
-consts whn :: hypnat
-
-defs
+definition
   (* omega is in fact an infinite hypernatural number = [<1,2,3,...>] *)
-  hypnat_omega_def:  "whn == star_n (%n::nat. n)"
+  whn :: hypnat
+  hypnat_omega_def: "whn = star_n (%n::nat. n)"
 
 text{*Existence of infinite number not corresponding to any natural number
 follows because member @{term FreeUltrafilterNat} is not finite.
@@ -201,11 +200,10 @@
 
 subsection{*Infinite Hypernatural Numbers -- @{term HNatInfinite}*}
 
-constdefs
-
+definition
   (* the set of infinite hypernatural numbers *)
   HNatInfinite :: "hypnat set"
-  "HNatInfinite == {n. n \<notin> Nats}"
+  "HNatInfinite = {n. n \<notin> Nats}"
 
 lemma HNatInfinite_whn [simp]: "whn \<in> HNatInfinite"
 by (simp add: HNatInfinite_def)
@@ -327,9 +325,9 @@
 subsection{*Embedding of the Hypernaturals into the Hyperreals*}
 text{*Obtained using the nonstandard extension of the naturals*}
 
-constdefs
+definition
   hypreal_of_hypnat :: "hypnat => hypreal"
-   "hypreal_of_hypnat == *f* real"
+  "hypreal_of_hypnat = *f* real"
 
 declare hypreal_of_hypnat_def [transfer_unfold]
 
@@ -384,73 +382,4 @@
 apply (simp add: hypreal_of_hypnat_zero [symmetric] linorder_not_less)
 done
 
-
-ML
-{*
-val hypnat_of_nat_def = thm"hypnat_of_nat_def";
-val HNatInfinite_def = thm"HNatInfinite_def";
-val hypreal_of_hypnat_def = thm"hypreal_of_hypnat_def";
-val hypnat_omega_def = thm"hypnat_omega_def";
-
-val starrel_iff = thm "starrel_iff";
-val lemma_starrel_refl = thm "lemma_starrel_refl";
-val hypnat_minus_zero = thm "hypnat_minus_zero";
-val hypnat_diff_0_eq_0 = thm "hypnat_diff_0_eq_0";
-val hypnat_add_is_0 = thm "hypnat_add_is_0";
-val hypnat_diff_diff_left = thm "hypnat_diff_diff_left";
-val hypnat_diff_commute = thm "hypnat_diff_commute";
-val hypnat_diff_add_inverse = thm "hypnat_diff_add_inverse";
-val hypnat_diff_add_inverse2 = thm "hypnat_diff_add_inverse2";
-val hypnat_diff_cancel = thm "hypnat_diff_cancel";
-val hypnat_diff_cancel2 = thm "hypnat_diff_cancel2";
-val hypnat_diff_add_0 = thm "hypnat_diff_add_0";
-val hypnat_diff_mult_distrib = thm "hypnat_diff_mult_distrib";
-val hypnat_diff_mult_distrib2 = thm "hypnat_diff_mult_distrib2";
-val hypnat_mult_is_0 = thm "hypnat_mult_is_0";
-val hypnat_not_less0 = thm "hypnat_not_less0";
-val hypnat_less_one = thm "hypnat_less_one";
-val hypnat_add_diff_inverse = thm "hypnat_add_diff_inverse";
-val hypnat_le_add_diff_inverse = thm "hypnat_le_add_diff_inverse";
-val hypnat_le_add_diff_inverse2 = thm "hypnat_le_add_diff_inverse2";
-val hypnat_le0 = thm "hypnat_le0";
-val hypnat_add_self_le = thm "hypnat_add_self_le";
-val hypnat_add_one_self_less = thm "hypnat_add_one_self_less";
-val hypnat_neq0_conv = thm "hypnat_neq0_conv";
-val hypnat_gt_zero_iff = thm "hypnat_gt_zero_iff";
-val hypnat_gt_zero_iff2 = thm "hypnat_gt_zero_iff2";
-val SHNat_eq = thm"SHNat_eq"
-val hypnat_of_nat_one = thm "hypnat_of_nat_one";
-val hypnat_of_nat_Suc = thm "hypnat_of_nat_Suc";
-val SHNAT_omega_not_mem = thm "SHNAT_omega_not_mem";
-val cofinite_mem_FreeUltrafilterNat = thm "cofinite_mem_FreeUltrafilterNat";
-val hypnat_omega_gt_SHNat = thm "hypnat_omega_gt_SHNat";
-val hypnat_of_nat_less_whn = thm "hypnat_of_nat_less_whn";
-val hypnat_of_nat_le_whn = thm "hypnat_of_nat_le_whn";
-val hypnat_zero_less_hypnat_omega = thm "hypnat_zero_less_hypnat_omega";
-val hypnat_one_less_hypnat_omega = thm "hypnat_one_less_hypnat_omega";
-val HNatInfinite_whn = thm "HNatInfinite_whn";
-val HNatInfinite_iff = thm "HNatInfinite_iff";
-val HNatInfinite_FreeUltrafilterNat = thm "HNatInfinite_FreeUltrafilterNat";
-val FreeUltrafilterNat_HNatInfinite = thm "FreeUltrafilterNat_HNatInfinite";
-val HNatInfinite_FreeUltrafilterNat_iff = thm "HNatInfinite_FreeUltrafilterNat_iff";
-val HNatInfinite_gt_one = thm "HNatInfinite_gt_one";
-val zero_not_mem_HNatInfinite = thm "zero_not_mem_HNatInfinite";
-val HNatInfinite_not_eq_zero = thm "HNatInfinite_not_eq_zero";
-val HNatInfinite_ge_one = thm "HNatInfinite_ge_one";
-val HNatInfinite_add = thm "HNatInfinite_add";
-val HNatInfinite_SHNat_add = thm "HNatInfinite_SHNat_add";
-val HNatInfinite_SHNat_diff = thm "HNatInfinite_SHNat_diff";
-val HNatInfinite_add_one = thm "HNatInfinite_add_one";
-val HNatInfinite_is_Suc = thm "HNatInfinite_is_Suc";
-val HNat_hypreal_of_nat = thm "HNat_hypreal_of_nat";
-val hypreal_of_hypnat = thm "hypreal_of_hypnat";
-val hypreal_of_hypnat_zero = thm "hypreal_of_hypnat_zero";
-val hypreal_of_hypnat_one = thm "hypreal_of_hypnat_one";
-val hypreal_of_hypnat_add = thm "hypreal_of_hypnat_add";
-val hypreal_of_hypnat_mult = thm "hypreal_of_hypnat_mult";
-val hypreal_of_hypnat_less_iff = thm "hypreal_of_hypnat_less_iff";
-val hypreal_of_hypnat_ge_zero = thm "hypreal_of_hypnat_ge_zero";
-val HNatInfinite_inverse_Infinitesimal = thm "HNatInfinite_inverse_Infinitesimal";
-*}
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/HyperPow.thy
--- a/src/HOL/Hyperreal/HyperPow.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/HyperPow.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -18,14 +18,11 @@
 lemma hpowr_Suc [simp]: "r ^ (Suc n) = (r::hypreal) * (r ^ n)"
 by (rule power_Suc)
 
-consts
-  "pow"  :: "[hypreal,hypnat] => hypreal"     (infixr "pow" 80)
-
-defs
-
+definition
   (* hypernatural powers of hyperreals *)
+  pow :: "[hypreal,hypnat] => hypreal"     (infixr "pow" 80)
   hyperpow_def [transfer_unfold]:
-  "(R::hypreal) pow (N::hypnat) == ( *f2* op ^) R N"
+  "(R::hypreal) pow (N::hypnat) = ( *f2* op ^) R N"
 
 lemma hrealpow_two: "(r::hypreal) ^ Suc (Suc 0) = r * r"
 by simp
@@ -235,54 +232,4 @@
      "[| x \<in> Infinitesimal; 0 < n |] ==> x ^ n \<in> Infinitesimal"
 by (simp add: hrealpow_hyperpow_Infinitesimal_iff Infinitesimal_hyperpow)
 
-ML
-{*
-val hrealpow_two = thm "hrealpow_two";
-val hrealpow_two_le = thm "hrealpow_two_le";
-val hrealpow_two_le_add_order = thm "hrealpow_two_le_add_order";
-val hrealpow_two_le_add_order2 = thm "hrealpow_two_le_add_order2";
-val hypreal_add_nonneg_eq_0_iff = thm "hypreal_add_nonneg_eq_0_iff";
-val hypreal_three_squares_add_zero_iff = thm "hypreal_three_squares_add_zero_iff";
-val hrealpow_three_squares_add_zero_iff = thm "hrealpow_three_squares_add_zero_iff";
-val hrabs_hrealpow_two = thm "hrabs_hrealpow_two";
-val two_hrealpow_ge_one = thm "two_hrealpow_ge_one";
-val two_hrealpow_gt = thm "two_hrealpow_gt";
-val hrealpow = thm "hrealpow";
-val hrealpow_sum_square_expand = thm "hrealpow_sum_square_expand";
-val power_hypreal_of_real_number_of = thm "power_hypreal_of_real_number_of";
-val hrealpow_HFinite = thm "hrealpow_HFinite";
-val hyperpow = thm "hyperpow";
-val hyperpow_zero = thm "hyperpow_zero";
-val hyperpow_not_zero = thm "hyperpow_not_zero";
-val hyperpow_inverse = thm "hyperpow_inverse";
-val hyperpow_hrabs = thm "hyperpow_hrabs";
-val hyperpow_add = thm "hyperpow_add";
-val hyperpow_one = thm "hyperpow_one";
-val hyperpow_two = thm "hyperpow_two";
-val hyperpow_gt_zero = thm "hyperpow_gt_zero";
-val hyperpow_ge_zero = thm "hyperpow_ge_zero";
-val hyperpow_le = thm "hyperpow_le";
-val hyperpow_eq_one = thm "hyperpow_eq_one";
-val hrabs_hyperpow_minus_one = thm "hrabs_hyperpow_minus_one";
-val hyperpow_mult = thm "hyperpow_mult";
-val hyperpow_two_le = thm "hyperpow_two_le";
-val hrabs_hyperpow_two = thm "hrabs_hyperpow_two";
-val hyperpow_two_hrabs = thm "hyperpow_two_hrabs";
-val hyperpow_two_gt_one = thm "hyperpow_two_gt_one";
-val hyperpow_two_ge_one = thm "hyperpow_two_ge_one";
-val two_hyperpow_ge_one = thm "two_hyperpow_ge_one";
-val hyperpow_minus_one2 = thm "hyperpow_minus_one2";
-val hyperpow_less_le = thm "hyperpow_less_le";
-val hyperpow_SHNat_le = thm "hyperpow_SHNat_le";
-val hyperpow_realpow = thm "hyperpow_realpow";
-val hyperpow_SReal = thm "hyperpow_SReal";
-val hyperpow_zero_HNatInfinite = thm "hyperpow_zero_HNatInfinite";
-val hyperpow_le_le = thm "hyperpow_le_le";
-val hyperpow_Suc_le_self2 = thm "hyperpow_Suc_le_self2";
-val lemma_Infinitesimal_hyperpow = thm "lemma_Infinitesimal_hyperpow";
-val Infinitesimal_hyperpow = thm "Infinitesimal_hyperpow";
-val hrealpow_hyperpow_Infinitesimal_iff = thm "hrealpow_hyperpow_Infinitesimal_iff";
-val Infinitesimal_hrealpow = thm "Infinitesimal_hrealpow";
-*}
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/Integration.thy
--- a/src/HOL/Hyperreal/Integration.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/Integration.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -12,43 +12,43 @@
 
 text{*We follow John Harrison in formalizing the Gauge integral.*}
 
-constdefs
+definition
 
   --{*Partitions and tagged partitions etc.*}
 
   partition :: "[(real*real),nat => real] => bool"
-  "partition == %(a,b) D. D 0 = a &
+  "partition = (%(a,b) D. D 0 = a &
                          (\<exists>N. (\<forall>n < N. D(n) < D(Suc n)) &
-                              (\<forall>n \<ge> N. D(n) = b))"
+                              (\<forall>n \<ge> N. D(n) = b)))"
 
   psize :: "(nat => real) => nat"
-  "psize D == SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
-                      (\<forall>n \<ge> N. D(n) = D(N))"
+  "psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
+                      (\<forall>n \<ge> N. D(n) = D(N)))"
 
   tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool"
-  "tpart == %(a,b) (D,p). partition(a,b) D &
-                          (\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n))"
+  "tpart = (%(a,b) (D,p). partition(a,b) D &
+                          (\<forall>n. D(n) \<le> p(n) & p(n) \<le> D(Suc n)))"
 
   --{*Gauges and gauge-fine divisions*}
 
   gauge :: "[real => bool, real => real] => bool"
-  "gauge E g == \<forall>x. E x --> 0 < g(x)"
+  "gauge E g = (\<forall>x. E x --> 0 < g(x))"
 
   fine :: "[real => real, ((nat => real)*(nat => real))] => bool"
-  "fine == % g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n)"
+  "fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))"
 
   --{*Riemann sum*}
 
   rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real"
-  "rsum == %(D,p) f. \<Sum>n=0..<psize(D). f(p n) * (D(Suc n) - D(n))"
+  "rsum = (%(D,p) f. \<Sum>n=0..<psize(D). f(p n) * (D(Suc n) - D(n)))"
 
   --{*Gauge integrability (definite)*}
 
-   Integral :: "[(real*real),real=>real,real] => bool"
-   "Integral == %(a,b) f k. \<forall>e > 0.
+  Integral :: "[(real*real),real=>real,real] => bool"
+  "Integral = (%(a,b) f k. \<forall>e > 0.
                                (\<exists>g. gauge(%x. a \<le> x & x \<le> b) g &
                                (\<forall>D p. tpart(a,b) (D,p) & fine(g)(D,p) -->
-                                         \<bar>rsum(D,p) f - k\<bar> < e))"
+                                         \<bar>rsum(D,p) f - k\<bar> < e)))"
 
 
 lemma partition_zero [simp]: "a = b ==> psize (%n. if n = 0 then a else b) = 0"
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -14,61 +14,58 @@
 
 text{*Standard and Nonstandard Definitions*}
 
-constdefs
+definition
   LIM :: "[real=>real,real,real] => bool"
         ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60)
-  "f -- a --> L ==
-     \<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s
-        --> \<bar>f x + -L\<bar> < r"
+  "f -- a --> L =
+     (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & \<bar>x + -a\<bar> < s
+        --> \<bar>f x + -L\<bar> < r)"
 
   NSLIM :: "[real=>real,real,real] => bool"
             ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60)
-  "f -- a --NS> L == (\<forall>x. (x \<noteq> hypreal_of_real a &
+  "f -- a --NS> L = (\<forall>x. (x \<noteq> hypreal_of_real a &
           x @= hypreal_of_real a -->
           ( *f* f) x @= hypreal_of_real L))"
 
   isCont :: "[real=>real,real] => bool"
-  "isCont f a == (f -- a --> (f a))"
+  "isCont f a = (f -- a --> (f a))"
 
   isNSCont :: "[real=>real,real] => bool"
     --{*NS definition dispenses with limit notions*}
-  "isNSCont f a == (\<forall>y. y @= hypreal_of_real a -->
+  "isNSCont f a = (\<forall>y. y @= hypreal_of_real a -->
          ( *f* f) y @= hypreal_of_real (f a))"
 
   deriv:: "[real=>real,real,real] => bool"
     --{*Differentiation: D is derivative of function f at x*}
           ("(DERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
-  "DERIV f x :> D == ((%h. (f(x + h) + -f x)/h) -- 0 --> D)"
+  "DERIV f x :> D = ((%h. (f(x + h) + -f x)/h) -- 0 --> D)"
 
   nsderiv :: "[real=>real,real,real] => bool"
           ("(NSDERIV (_)/ (_)/ :> (_))" [1000, 1000, 60] 60)
-  "NSDERIV f x :> D == (\<forall>h \<in> Infinitesimal - {0}.
+  "NSDERIV f x :> D = (\<forall>h \<in> Infinitesimal - {0}.
       (( *f* f)(hypreal_of_real x + h) +
        - hypreal_of_real (f x))/h @= hypreal_of_real D)"
 
   differentiable :: "[real=>real,real] => bool"   (infixl "differentiable" 60)
-  "f differentiable x == (\<exists>D. DERIV f x :> D)"
+  "f differentiable x = (\<exists>D. DERIV f x :> D)"
 
   NSdifferentiable :: "[real=>real,real] => bool"
                        (infixl "NSdifferentiable" 60)
-  "f NSdifferentiable x == (\<exists>D. NSDERIV f x :> D)"
+  "f NSdifferentiable x = (\<exists>D. NSDERIV f x :> D)"
 
   increment :: "[real=>real,real,hypreal] => hypreal"
-  "increment f x h == (@inc. f NSdifferentiable x &
+  "increment f x h = (@inc. f NSdifferentiable x &
            inc = ( *f* f)(hypreal_of_real x + h) + -hypreal_of_real (f x))"
 
   isUCont :: "(real=>real) => bool"
-  "isUCont f ==  \<forall>r > 0. \<exists>s > 0. \<forall>x y. \<bar>x + -y\<bar> < s --> \<bar>f x + -f y\<bar> < r"
+  "isUCont f =  (\<forall>r > 0. \<exists>s > 0. \<forall>x y. \<bar>x + -y\<bar> < s --> \<bar>f x + -f y\<bar> < r)"
 
   isNSUCont :: "(real=>real) => bool"
-  "isNSUCont f == (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
+  "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
 
 
 consts
   Bolzano_bisect :: "[real*real=>bool, real, real, nat] => (real*real)"
-    --{*Used in the proof of the Bolzano theorem*}
-
-
 primrec
   "Bolzano_bisect P a b 0 = (a,b)"
   "Bolzano_bisect P a b (Suc n) =
@@ -2372,202 +2369,4 @@
   thus ?thesis by (fold LIM_def)
 qed
 
-
-
-ML
-{*
-val LIM_def = thm"LIM_def";
-val NSLIM_def = thm"NSLIM_def";
-val isCont_def = thm"isCont_def";
-val isNSCont_def = thm"isNSCont_def";
-val deriv_def = thm"deriv_def";
-val nsderiv_def = thm"nsderiv_def";
-val differentiable_def = thm"differentiable_def";
-val NSdifferentiable_def = thm"NSdifferentiable_def";
-val increment_def = thm"increment_def";
-val isUCont_def = thm"isUCont_def";
-val isNSUCont_def = thm"isNSUCont_def";
-
-val half_gt_zero_iff = thm "half_gt_zero_iff";
-val half_gt_zero = thms "half_gt_zero";
-val abs_diff_triangle_ineq = thm "abs_diff_triangle_ineq";
-val LIM_eq = thm "LIM_eq";
-val LIM_D = thm "LIM_D";
-val LIM_const = thm "LIM_const";
-val LIM_add = thm "LIM_add";
-val LIM_minus = thm "LIM_minus";
-val LIM_add_minus = thm "LIM_add_minus";
-val LIM_diff = thm "LIM_diff";
-val LIM_const_not_eq = thm "LIM_const_not_eq";
-val LIM_const_eq = thm "LIM_const_eq";
-val LIM_unique = thm "LIM_unique";
-val LIM_mult_zero = thm "LIM_mult_zero";
-val LIM_self = thm "LIM_self";
-val LIM_equal = thm "LIM_equal";
-val LIM_trans = thm "LIM_trans";
-val LIM_NSLIM = thm "LIM_NSLIM";
-val NSLIM_LIM = thm "NSLIM_LIM";
-val LIM_NSLIM_iff = thm "LIM_NSLIM_iff";
-val NSLIM_mult = thm "NSLIM_mult";
-val LIM_mult2 = thm "LIM_mult2";
-val NSLIM_add = thm "NSLIM_add";
-val LIM_add2 = thm "LIM_add2";
-val NSLIM_const = thm "NSLIM_const";
-val LIM_const2 = thm "LIM_const2";
-val NSLIM_minus = thm "NSLIM_minus";
-val LIM_minus2 = thm "LIM_minus2";
-val NSLIM_add_minus = thm "NSLIM_add_minus";
-val LIM_add_minus2 = thm "LIM_add_minus2";
-val NSLIM_inverse = thm "NSLIM_inverse";
-val LIM_inverse = thm "LIM_inverse";
-val NSLIM_zero = thm "NSLIM_zero";
-val LIM_zero2 = thm "LIM_zero2";
-val NSLIM_zero_cancel = thm "NSLIM_zero_cancel";
-val LIM_zero_cancel = thm "LIM_zero_cancel";
-val NSLIM_not_zero = thm "NSLIM_not_zero";
-val NSLIM_const_not_eq = thm "NSLIM_const_not_eq";
-val NSLIM_const_eq = thm "NSLIM_const_eq";
-val NSLIM_unique = thm "NSLIM_unique";
-val LIM_unique2 = thm "LIM_unique2";
-val NSLIM_mult_zero = thm "NSLIM_mult_zero";
-val LIM_mult_zero2 = thm "LIM_mult_zero2";
-val NSLIM_self = thm "NSLIM_self";
-val isNSContD = thm "isNSContD";
-val isNSCont_NSLIM = thm "isNSCont_NSLIM";
-val NSLIM_isNSCont = thm "NSLIM_isNSCont";
-val isNSCont_NSLIM_iff = thm "isNSCont_NSLIM_iff";
-val isNSCont_LIM_iff = thm "isNSCont_LIM_iff";
-val isNSCont_isCont_iff = thm "isNSCont_isCont_iff";
-val isCont_isNSCont = thm "isCont_isNSCont";
-val isNSCont_isCont = thm "isNSCont_isCont";
-val NSLIM_h_iff = thm "NSLIM_h_iff";
-val NSLIM_isCont_iff = thm "NSLIM_isCont_iff";
-val LIM_isCont_iff = thm "LIM_isCont_iff";
-val isCont_iff = thm "isCont_iff";
-val isCont_add = thm "isCont_add";
-val isCont_mult = thm "isCont_mult";
-val isCont_o = thm "isCont_o";
-val isCont_o2 = thm "isCont_o2";
-val isNSCont_minus = thm "isNSCont_minus";
-val isCont_minus = thm "isCont_minus";
-val isCont_inverse = thm "isCont_inverse";
-val isNSCont_inverse = thm "isNSCont_inverse";
-val isCont_diff = thm "isCont_diff";
-val isCont_const = thm "isCont_const";
-val isNSCont_const = thm "isNSCont_const";
-val isNSUContD = thm "isNSUContD";
-val isUCont_isCont = thm "isUCont_isCont";
-val isUCont_isNSUCont = thm "isUCont_isNSUCont";
-val isNSUCont_isUCont = thm "isNSUCont_isUCont";
-val DERIV_iff = thm "DERIV_iff";
-val DERIV_NS_iff = thm "DERIV_NS_iff";
-val DERIV_D = thm "DERIV_D";
-val NS_DERIV_D = thm "NS_DERIV_D";
-val DERIV_unique = thm "DERIV_unique";
-val NSDeriv_unique = thm "NSDeriv_unique";
-val differentiableD = thm "differentiableD";
-val differentiableI = thm "differentiableI";
-val NSdifferentiableD = thm "NSdifferentiableD";
-val NSdifferentiableI = thm "NSdifferentiableI";
-val LIM_I = thm "LIM_I";
-val DERIV_LIM_iff = thm "DERIV_LIM_iff";
-val DERIV_iff2 = thm "DERIV_iff2";
-val NSDERIV_NSLIM_iff = thm "NSDERIV_NSLIM_iff";
-val NSDERIV_NSLIM_iff2 = thm "NSDERIV_NSLIM_iff2";
-val NSDERIV_iff2 = thm "NSDERIV_iff2";
-val hypreal_not_eq_minus_iff = thm "hypreal_not_eq_minus_iff";
-val NSDERIVD5 = thm "NSDERIVD5";
-val NSDERIVD4 = thm "NSDERIVD4";
-val NSDERIVD3 = thm "NSDERIVD3";
-val NSDERIV_DERIV_iff = thm "NSDERIV_DERIV_iff";
-val NSDERIV_isNSCont = thm "NSDERIV_isNSCont";
-val DERIV_isCont = thm "DERIV_isCont";
-val NSDERIV_const = thm "NSDERIV_const";
-val DERIV_const = thm "DERIV_const";
-val NSDERIV_add = thm "NSDERIV_add";
-val DERIV_add = thm "DERIV_add";
-val NSDERIV_mult = thm "NSDERIV_mult";
-val DERIV_mult = thm "DERIV_mult";
-val NSDERIV_cmult = thm "NSDERIV_cmult";
-val DERIV_cmult = thm "DERIV_cmult";
-val NSDERIV_minus = thm "NSDERIV_minus";
-val DERIV_minus = thm "DERIV_minus";
-val NSDERIV_add_minus = thm "NSDERIV_add_minus";
-val DERIV_add_minus = thm "DERIV_add_minus";
-val NSDERIV_diff = thm "NSDERIV_diff";
-val DERIV_diff = thm "DERIV_diff";
-val incrementI = thm "incrementI";
-val incrementI2 = thm "incrementI2";
-val increment_thm = thm "increment_thm";
-val increment_thm2 = thm "increment_thm2";
-val increment_approx_zero = thm "increment_approx_zero";
-val NSDERIV_zero = thm "NSDERIV_zero";
-val NSDERIV_approx = thm "NSDERIV_approx";
-val NSDERIVD1 = thm "NSDERIVD1";
-val NSDERIVD2 = thm "NSDERIVD2";
-val NSDERIV_chain = thm "NSDERIV_chain";
-val DERIV_chain = thm "DERIV_chain";
-val DERIV_chain2 = thm "DERIV_chain2";
-val NSDERIV_Id = thm "NSDERIV_Id";
-val DERIV_Id = thm "DERIV_Id";
-val isCont_Id = thms "isCont_Id";
-val DERIV_cmult_Id = thm "DERIV_cmult_Id";
-val NSDERIV_cmult_Id = thm "NSDERIV_cmult_Id";
-val DERIV_pow = thm "DERIV_pow";
-val NSDERIV_pow = thm "NSDERIV_pow";
-val NSDERIV_inverse = thm "NSDERIV_inverse";
-val DERIV_inverse = thm "DERIV_inverse";
-val DERIV_inverse_fun = thm "DERIV_inverse_fun";
-val NSDERIV_inverse_fun = thm "NSDERIV_inverse_fun";
-val DERIV_quotient = thm "DERIV_quotient";
-val NSDERIV_quotient = thm "NSDERIV_quotient";
-val CARAT_DERIV = thm "CARAT_DERIV";
-val CARAT_NSDERIV = thm "CARAT_NSDERIV";
-val hypreal_eq_minus_iff3 = thm "hypreal_eq_minus_iff3";
-val starfun_if_eq = thm "starfun_if_eq";
-val CARAT_DERIVD = thm "CARAT_DERIVD";
-val f_inc_g_dec_Beq_f = thm "f_inc_g_dec_Beq_f";
-val f_inc_g_dec_Beq_g = thm "f_inc_g_dec_Beq_g";
-val f_inc_imp_le_lim = thm "f_inc_imp_le_lim";
-val lim_uminus = thm "lim_uminus";
-val g_dec_imp_lim_le = thm "g_dec_imp_lim_le";
-val Bolzano_bisect_le = thm "Bolzano_bisect_le";
-val Bolzano_bisect_fst_le_Suc = thm "Bolzano_bisect_fst_le_Suc";
-val Bolzano_bisect_Suc_le_snd = thm "Bolzano_bisect_Suc_le_snd";
-val eq_divide_2_times_iff = thm "eq_divide_2_times_iff";
-val Bolzano_bisect_diff = thm "Bolzano_bisect_diff";
-val Bolzano_nest_unique = thms "Bolzano_nest_unique";
-val not_P_Bolzano_bisect = thm "not_P_Bolzano_bisect";
-val not_P_Bolzano_bisect = thm "not_P_Bolzano_bisect";
-val lemma_BOLZANO2 = thm "lemma_BOLZANO2";
-val IVT = thm "IVT";
-val IVT2 = thm "IVT2";
-val IVT_objl = thm "IVT_objl";
-val IVT2_objl = thm "IVT2_objl";
-val isCont_bounded = thm "isCont_bounded";
-val isCont_has_Ub = thm "isCont_has_Ub";
-val isCont_eq_Ub = thm "isCont_eq_Ub";
-val isCont_eq_Lb = thm "isCont_eq_Lb";
-val isCont_Lb_Ub = thm "isCont_Lb_Ub";
-val DERIV_left_inc = thm "DERIV_left_inc";
-val DERIV_left_dec = thm "DERIV_left_dec";
-val DERIV_local_max = thm "DERIV_local_max";
-val DERIV_local_min = thm "DERIV_local_min";
-val DERIV_local_const = thm "DERIV_local_const";
-val Rolle = thm "Rolle";
-val MVT = thm "MVT";
-val DERIV_isconst_end = thm "DERIV_isconst_end";
-val DERIV_isconst1 = thm "DERIV_isconst1";
-val DERIV_isconst2 = thm "DERIV_isconst2";
-val DERIV_isconst_all = thm "DERIV_isconst_all";
-val DERIV_const_ratio_const = thm "DERIV_const_ratio_const";
-val DERIV_const_ratio_const2 = thm "DERIV_const_ratio_const2";
-val real_average_minus_first = thm "real_average_minus_first";
-val real_average_minus_second = thm "real_average_minus_second";
-val DERIV_const_average = thm "DERIV_const_average";
-val isCont_inj_range = thm "isCont_inj_range";
-val isCont_inverse_function = thm "isCont_inverse_function";
-*}
-
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/Ln.thy
--- a/src/HOL/Hyperreal/Ln.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/Ln.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -6,7 +6,6 @@
 header {* Properties of ln *}
 
 theory Ln
-
 imports Transcendental
 begin
 
@@ -14,7 +13,7 @@
   inverse(real (fact (n+2))) * (x ^ (n+2)))"
 proof -
   have "exp x = suminf (%n. inverse(real (fact n)) * (x ^ n))"
-    by (unfold exp_def, simp)
+    by (simp add: exp_def)
   also from summable_exp have "... = (SUM n : {0..<2}. 
       inverse(real (fact n)) * (x ^ n)) + suminf (%n.
       inverse(real (fact (n+2))) * (x ^ (n+2)))" (is "_ = ?a + _")
@@ -477,4 +476,3 @@
 qed
 
 end
-
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/Log.thy
--- a/src/HOL/Hyperreal/Log.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/Log.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -10,15 +10,14 @@
 imports Transcendental
 begin
 
-constdefs
-
+definition
   powr  :: "[real,real] => real"     (infixr "powr" 80)
     --{*exponentation with real exponent*}
-    "x powr a == exp(a * ln x)"
+  "x powr a = exp(a * ln x)"
 
   log :: "[real,real] => real"
     --{*logarithm of @{term x} to base @{term a}*}
-    "log a x == ln x / ln a"
+  "log a x = ln x / ln a"
 
 
 
@@ -273,39 +272,4 @@
     finally show "real n powr - s < r" .
   qed
 
-
-
-ML
-{*
-val powr_one_eq_one = thm "powr_one_eq_one";
-val powr_zero_eq_one = thm "powr_zero_eq_one";
-val powr_one_gt_zero_iff = thm "powr_one_gt_zero_iff";
-val powr_mult = thm "powr_mult";
-val powr_gt_zero = thm "powr_gt_zero";
-val powr_not_zero = thm "powr_not_zero";
-val powr_divide = thm "powr_divide";
-val powr_add = thm "powr_add";
-val powr_powr = thm "powr_powr";
-val powr_powr_swap = thm "powr_powr_swap";
-val powr_minus = thm "powr_minus";
-val powr_minus_divide = thm "powr_minus_divide";
-val powr_less_mono = thm "powr_less_mono";
-val powr_less_cancel = thm "powr_less_cancel";
-val powr_less_cancel_iff = thm "powr_less_cancel_iff";
-val powr_le_cancel_iff = thm "powr_le_cancel_iff";
-val log_ln = thm "log_ln";
-val powr_log_cancel = thm "powr_log_cancel";
-val log_powr_cancel = thm "log_powr_cancel";
-val log_mult = thm "log_mult";
-val log_eq_div_ln_mult_log = thm "log_eq_div_ln_mult_log";
-val log_base_10_eq1 = thm "log_base_10_eq1";
-val log_base_10_eq2 = thm "log_base_10_eq2";
-val log_one = thm "log_one";
-val log_eq_one = thm "log_eq_one";
-val log_inverse = thm "log_inverse";
-val log_divide = thm "log_divide";
-val log_less_cancel_iff = thm "log_less_cancel_iff";
-val log_le_cancel_iff = thm "log_le_cancel_iff";
-*}
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -31,18 +31,24 @@
 text{*A crude tactic to differentiate by proof.*}
 ML
 {*
+local
+val deriv_rulesI =
+  [thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos", thm "DERIV_cmult",
+  thm "DERIV_sin", thm "DERIV_exp", thm "DERIV_inverse", thm "DERIV_pow",
+  thm "DERIV_add", thm "DERIV_diff", thm "DERIV_mult", thm "DERIV_minus",
+  thm "DERIV_inverse_fun", thm "DERIV_quotient", thm "DERIV_fun_pow",
+  thm "DERIV_fun_exp", thm "DERIV_fun_sin", thm "DERIV_fun_cos",
+  thm "DERIV_Id", thm "DERIV_const", thm "DERIV_cos"];
+
+val DERIV_chain2 = thm "DERIV_chain2";
+
+in
+
 exception DERIV_name;
 fun get_fun_name (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _)) = f
 |   get_fun_name (_ $ (_ $ (Const ("Lim.deriv",_) $ Abs(_,_, Const (f,_) $ _) $ _ $ _))) = f
 |   get_fun_name _ = raise DERIV_name;
 
-val deriv_rulesI = [DERIV_Id,DERIV_const,DERIV_cos,DERIV_cmult,
-                    DERIV_sin, DERIV_exp, DERIV_inverse,DERIV_pow,
-                    DERIV_add, DERIV_diff, DERIV_mult, DERIV_minus,
-                    DERIV_inverse_fun,DERIV_quotient,DERIV_fun_pow,
-                    DERIV_fun_exp,DERIV_fun_sin,DERIV_fun_cos,
-                    DERIV_Id,DERIV_const,DERIV_cos];
-
 val deriv_tac =
   SUBGOAL (fn (prem,i) =>
    (resolve_tac deriv_rulesI i) ORELSE
@@ -50,6 +56,8 @@
                      DERIV_chain2) i) handle DERIV_name => no_tac));;
 
 val DERIV_tac = ALLGOALS(fn i => REPEAT(deriv_tac i));
+
+end
 *}
 
 lemma Maclaurin_lemma2:
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -11,42 +11,41 @@
 imports HyperArith "../Real/RComplete"
 begin
 
-constdefs
+definition
 
   Infinitesimal  :: "hypreal set"
-   "Infinitesimal == {x. \<forall>r \<in> Reals. 0 < r --> abs x < r}"
+  "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> abs x < r}"
 
   HFinite :: "hypreal set"
-   "HFinite == {x. \<exists>r \<in> Reals. abs x < r}"
+  "HFinite = {x. \<exists>r \<in> Reals. abs x < r}"
 
   HInfinite :: "hypreal set"
-   "HInfinite == {x. \<forall>r \<in> Reals. r < abs x}"
+  "HInfinite = {x. \<forall>r \<in> Reals. r < abs x}"
 
   approx :: "[hypreal, hypreal] => bool"    (infixl "@=" 50)
     --{*the `infinitely close' relation*}
-   "x @= y       == (x + -y) \<in> Infinitesimal"
+  "(x @= y) = ((x + -y) \<in> Infinitesimal)"
 
   st        :: "hypreal => hypreal"
     --{*the standard part of a hyperreal*}
-   "st           == (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"
+  "st = (%x. @r. x \<in> HFinite & r \<in> Reals & r @= x)"
 
   monad     :: "hypreal => hypreal set"
-   "monad x      == {y. x @= y}"
+  "monad x = {y. x @= y}"
 
   galaxy    :: "hypreal => hypreal set"
-   "galaxy x     == {y. (x + -y) \<in> HFinite}"
+  "galaxy x = {y. (x + -y) \<in> HFinite}"
+
+const_syntax (xsymbols)
+  approx  (infixl "\<approx>" 50)
+
+const_syntax (HTML output)
+  approx  (infixl "\<approx>" 50)
 
 
 defs (overloaded)
-
-   SReal_def:      "Reals == {x. \<exists>r. x = hypreal_of_real r}"
-     --{*the standard real numbers as a subset of the hyperreals*}
-
-syntax (xsymbols)
-    approx :: "[hypreal, hypreal] => bool"    (infixl "\<approx>" 50)
-
-syntax (HTML output)
-    approx :: "[hypreal, hypreal] => bool"    (infixl "\<approx>" 50)
+  SReal_def:      "Reals == {x. \<exists>r. x = hypreal_of_real r}"
+    --{*the standard real numbers as a subset of the hyperreals*}
 
 
 
@@ -507,101 +506,16 @@
 by (blast intro: approx_sym)
 
 
-ML
-{*
-val SReal_add = thm "SReal_add";
-val SReal_mult = thm "SReal_mult";
-val SReal_inverse = thm "SReal_inverse";
-val SReal_divide = thm "SReal_divide";
-val SReal_minus = thm "SReal_minus";
-val SReal_minus_iff = thm "SReal_minus_iff";
-val SReal_add_cancel = thm "SReal_add_cancel";
-val SReal_hrabs = thm "SReal_hrabs";
-val SReal_hypreal_of_real = thm "SReal_hypreal_of_real";
-val SReal_number_of = thm "SReal_number_of";
-val Reals_0 = thm "Reals_0";
-val Reals_1 = thm "Reals_1";
-val SReal_divide_number_of = thm "SReal_divide_number_of";
-val SReal_epsilon_not_mem = thm "SReal_epsilon_not_mem";
-val SReal_omega_not_mem = thm "SReal_omega_not_mem";
-val SReal_UNIV_real = thm "SReal_UNIV_real";
-val SReal_iff = thm "SReal_iff";
-val hypreal_of_real_image = thm "hypreal_of_real_image";
-val inv_hypreal_of_real_image = thm "inv_hypreal_of_real_image";
-val SReal_hypreal_of_real_image = thm "SReal_hypreal_of_real_image";
-val SReal_dense = thm "SReal_dense";
-val hypreal_of_real_isUb_iff = thm "hypreal_of_real_isUb_iff";
-val hypreal_of_real_isLub1 = thm "hypreal_of_real_isLub1";
-val hypreal_of_real_isLub2 = thm "hypreal_of_real_isLub2";
-val hypreal_of_real_isLub_iff = thm "hypreal_of_real_isLub_iff";
-val lemma_isUb_hypreal_of_real = thm "lemma_isUb_hypreal_of_real";
-val lemma_isLub_hypreal_of_real = thm "lemma_isLub_hypreal_of_real";
-val lemma_isLub_hypreal_of_real2 = thm "lemma_isLub_hypreal_of_real2";
-val SReal_complete = thm "SReal_complete";
-val HFinite_add = thm "HFinite_add";
-val HFinite_mult = thm "HFinite_mult";
-val HFinite_minus_iff = thm "HFinite_minus_iff";
-val SReal_subset_HFinite = thm "SReal_subset_HFinite";
-val HFinite_hypreal_of_real = thm "HFinite_hypreal_of_real";
-val HFiniteD = thm "HFiniteD";
-val HFinite_hrabs_iff = thm "HFinite_hrabs_iff";
-val HFinite_number_of = thm "HFinite_number_of";
-val HFinite_0 = thm "HFinite_0";
-val HFinite_1 = thm "HFinite_1";
-val HFinite_bounded = thm "HFinite_bounded";
-val InfinitesimalD = thm "InfinitesimalD";
-val Infinitesimal_zero = thm "Infinitesimal_zero";
-val hypreal_sum_of_halves = thm "hypreal_sum_of_halves";
-val Infinitesimal_add = thm "Infinitesimal_add";
-val Infinitesimal_minus_iff = thm "Infinitesimal_minus_iff";
-val Infinitesimal_diff = thm "Infinitesimal_diff";
-val Infinitesimal_mult = thm "Infinitesimal_mult";
-val Infinitesimal_HFinite_mult = thm "Infinitesimal_HFinite_mult";
-val Infinitesimal_HFinite_mult2 = thm "Infinitesimal_HFinite_mult2";
-val HInfinite_inverse_Infinitesimal = thm "HInfinite_inverse_Infinitesimal";
-val HInfinite_mult = thm "HInfinite_mult";
-val HInfinite_add_ge_zero = thm "HInfinite_add_ge_zero";
-val HInfinite_add_ge_zero2 = thm "HInfinite_add_ge_zero2";
-val HInfinite_add_gt_zero = thm "HInfinite_add_gt_zero";
-val HInfinite_minus_iff = thm "HInfinite_minus_iff";
-val HInfinite_add_le_zero = thm "HInfinite_add_le_zero";
-val HInfinite_add_lt_zero = thm "HInfinite_add_lt_zero";
-val HFinite_sum_squares = thm "HFinite_sum_squares";
-val not_Infinitesimal_not_zero = thm "not_Infinitesimal_not_zero";
-val not_Infinitesimal_not_zero2 = thm "not_Infinitesimal_not_zero2";
-val Infinitesimal_hrabs_iff = thm "Infinitesimal_hrabs_iff";
-val HFinite_diff_Infinitesimal_hrabs = thm "HFinite_diff_Infinitesimal_hrabs";
-val hrabs_less_Infinitesimal = thm "hrabs_less_Infinitesimal";
-val hrabs_le_Infinitesimal = thm "hrabs_le_Infinitesimal";
-val Infinitesimal_interval = thm "Infinitesimal_interval";
-val Infinitesimal_interval2 = thm "Infinitesimal_interval2";
-val not_Infinitesimal_mult = thm "not_Infinitesimal_mult";
-val Infinitesimal_mult_disj = thm "Infinitesimal_mult_disj";
-val HFinite_Infinitesimal_not_zero = thm "HFinite_Infinitesimal_not_zero";
-val HFinite_Infinitesimal_diff_mult = thm "HFinite_Infinitesimal_diff_mult";
-val Infinitesimal_subset_HFinite = thm "Infinitesimal_subset_HFinite";
-val Infinitesimal_hypreal_of_real_mult = thm "Infinitesimal_hypreal_of_real_mult";
-val Infinitesimal_hypreal_of_real_mult2 = thm "Infinitesimal_hypreal_of_real_mult2";
-val mem_infmal_iff = thm "mem_infmal_iff";
-val approx_minus_iff = thm "approx_minus_iff";
-val approx_minus_iff2 = thm "approx_minus_iff2";
-val approx_refl = thm "approx_refl";
-val approx_sym = thm "approx_sym";
-val approx_trans = thm "approx_trans";
-val approx_trans2 = thm "approx_trans2";
-val approx_trans3 = thm "approx_trans3";
-val number_of_approx_reorient = thm "number_of_approx_reorient";
-val zero_approx_reorient = thm "zero_approx_reorient";
-val one_approx_reorient = thm "one_approx_reorient";
-
+ML {*
+local
 (*** re-orientation, following HOL/Integ/Bin.ML
      We re-orient x @=y where x is 0, 1 or a numeral, unless y is as well!
  ***)
 
 (*reorientation simprules using ==, for the following simproc*)
-val meta_zero_approx_reorient = zero_approx_reorient RS eq_reflection;
-val meta_one_approx_reorient = one_approx_reorient RS eq_reflection;
-val meta_number_of_approx_reorient = number_of_approx_reorient RS eq_reflection
+val meta_zero_approx_reorient = thm "zero_approx_reorient" RS eq_reflection;
+val meta_one_approx_reorient = thm "one_approx_reorient" RS eq_reflection;
+val meta_number_of_approx_reorient = thm "number_of_approx_reorient" RS eq_reflection
 
 (*reorientation simplification procedure: reorients (polymorphic)
   0 = x, 1 = x, nnn = x provided x isn't 0, 1 or a numeral.*)
@@ -616,9 +530,11 @@
               | Const("Numeral.number_of", _) $ _ =>
                                  meta_number_of_approx_reorient);
 
+in
 val approx_reorient_simproc =
   Bin_Simprocs.prep_simproc
     ("reorient_simproc", ["0@=x", "1@=x", "number_of w @= x"], reorient_proc);
+end;
 
 Addsimprocs [approx_reorient_simproc];
 *}
@@ -2147,213 +2063,4 @@
 	 simp add: Infinitesimal_FreeUltrafilterNat_iff star_n_minus 
                    star_n_add star_n_inverse)
 
-
-ML
-{*
-val Infinitesimal_def = thm"Infinitesimal_def";
-val HFinite_def = thm"HFinite_def";
-val HInfinite_def = thm"HInfinite_def";
-val st_def = thm"st_def";
-val monad_def = thm"monad_def";
-val galaxy_def = thm"galaxy_def";
-val approx_def = thm"approx_def";
-val SReal_def = thm"SReal_def";
-
-val Infinitesimal_approx_minus = thm "Infinitesimal_approx_minus";
-val approx_monad_iff = thm "approx_monad_iff";
-val Infinitesimal_approx = thm "Infinitesimal_approx";
-val approx_add = thm "approx_add";
-val approx_minus = thm "approx_minus";
-val approx_minus2 = thm "approx_minus2";
-val approx_minus_cancel = thm "approx_minus_cancel";
-val approx_add_minus = thm "approx_add_minus";
-val approx_mult1 = thm "approx_mult1";
-val approx_mult2 = thm "approx_mult2";
-val approx_mult_subst = thm "approx_mult_subst";
-val approx_mult_subst2 = thm "approx_mult_subst2";
-val approx_mult_subst_SReal = thm "approx_mult_subst_SReal";
-val approx_eq_imp = thm "approx_eq_imp";
-val Infinitesimal_minus_approx = thm "Infinitesimal_minus_approx";
-val bex_Infinitesimal_iff = thm "bex_Infinitesimal_iff";
-val bex_Infinitesimal_iff2 = thm "bex_Infinitesimal_iff2";
-val Infinitesimal_add_approx = thm "Infinitesimal_add_approx";
-val Infinitesimal_add_approx_self = thm "Infinitesimal_add_approx_self";
-val Infinitesimal_add_approx_self2 = thm "Infinitesimal_add_approx_self2";
-val Infinitesimal_add_minus_approx_self = thm "Infinitesimal_add_minus_approx_self";
-val Infinitesimal_add_cancel = thm "Infinitesimal_add_cancel";
-val Infinitesimal_add_right_cancel = thm "Infinitesimal_add_right_cancel";
-val approx_add_left_cancel = thm "approx_add_left_cancel";
-val approx_add_right_cancel = thm "approx_add_right_cancel";
-val approx_add_mono1 = thm "approx_add_mono1";
-val approx_add_mono2 = thm "approx_add_mono2";
-val approx_add_left_iff = thm "approx_add_left_iff";
-val approx_add_right_iff = thm "approx_add_right_iff";
-val approx_HFinite = thm "approx_HFinite";
-val approx_hypreal_of_real_HFinite = thm "approx_hypreal_of_real_HFinite";
-val approx_mult_HFinite = thm "approx_mult_HFinite";
-val approx_mult_hypreal_of_real = thm "approx_mult_hypreal_of_real";
-val approx_SReal_mult_cancel_zero = thm "approx_SReal_mult_cancel_zero";
-val approx_mult_SReal1 = thm "approx_mult_SReal1";
-val approx_mult_SReal2 = thm "approx_mult_SReal2";
-val approx_mult_SReal_zero_cancel_iff = thm "approx_mult_SReal_zero_cancel_iff";
-val approx_SReal_mult_cancel = thm "approx_SReal_mult_cancel";
-val approx_SReal_mult_cancel_iff1 = thm "approx_SReal_mult_cancel_iff1";
-val approx_le_bound = thm "approx_le_bound";
-val Infinitesimal_less_SReal = thm "Infinitesimal_less_SReal";
-val Infinitesimal_less_SReal2 = thm "Infinitesimal_less_SReal2";
-val SReal_not_Infinitesimal = thm "SReal_not_Infinitesimal";
-val SReal_minus_not_Infinitesimal = thm "SReal_minus_not_Infinitesimal";
-val SReal_Int_Infinitesimal_zero = thm "SReal_Int_Infinitesimal_zero";
-val SReal_Infinitesimal_zero = thm "SReal_Infinitesimal_zero";
-val SReal_HFinite_diff_Infinitesimal = thm "SReal_HFinite_diff_Infinitesimal";
-val hypreal_of_real_HFinite_diff_Infinitesimal = thm "hypreal_of_real_HFinite_diff_Infinitesimal";
-val hypreal_of_real_Infinitesimal_iff_0 = thm "hypreal_of_real_Infinitesimal_iff_0";
-val number_of_not_Infinitesimal = thm "number_of_not_Infinitesimal";
-val one_not_Infinitesimal = thm "one_not_Infinitesimal";
-val approx_SReal_not_zero = thm "approx_SReal_not_zero";
-val HFinite_diff_Infinitesimal_approx = thm "HFinite_diff_Infinitesimal_approx";
-val Infinitesimal_ratio = thm "Infinitesimal_ratio";
-val SReal_approx_iff = thm "SReal_approx_iff";
-val number_of_approx_iff = thm "number_of_approx_iff";
-val hypreal_of_real_approx_iff = thm "hypreal_of_real_approx_iff";
-val hypreal_of_real_approx_number_of_iff = thm "hypreal_of_real_approx_number_of_iff";
-val approx_unique_real = thm "approx_unique_real";
-val hypreal_isLub_unique = thm "hypreal_isLub_unique";
-val hypreal_setle_less_trans = thm "hypreal_setle_less_trans";
-val hypreal_gt_isUb = thm "hypreal_gt_isUb";
-val st_part_Ex = thm "st_part_Ex";
-val st_part_Ex1 = thm "st_part_Ex1";
-val HFinite_Int_HInfinite_empty = thm "HFinite_Int_HInfinite_empty";
-val HFinite_not_HInfinite = thm "HFinite_not_HInfinite";
-val not_HFinite_HInfinite = thm "not_HFinite_HInfinite";
-val HInfinite_HFinite_disj = thm "HInfinite_HFinite_disj";
-val HInfinite_HFinite_iff = thm "HInfinite_HFinite_iff";
-val HFinite_HInfinite_iff = thm "HFinite_HInfinite_iff";
-val HInfinite_diff_HFinite_Infinitesimal_disj = thm "HInfinite_diff_HFinite_Infinitesimal_disj";
-val HFinite_inverse = thm "HFinite_inverse";
-val HFinite_inverse2 = thm "HFinite_inverse2";
-val Infinitesimal_inverse_HFinite = thm "Infinitesimal_inverse_HFinite";
-val HFinite_not_Infinitesimal_inverse = thm "HFinite_not_Infinitesimal_inverse";
-val approx_inverse = thm "approx_inverse";
-val hypreal_of_real_approx_inverse = thm "hypreal_of_real_approx_inverse";
-val inverse_add_Infinitesimal_approx = thm "inverse_add_Infinitesimal_approx";
-val inverse_add_Infinitesimal_approx2 = thm "inverse_add_Infinitesimal_approx2";
-val inverse_add_Infinitesimal_approx_Infinitesimal = thm "inverse_add_Infinitesimal_approx_Infinitesimal";
-val Infinitesimal_square_iff = thm "Infinitesimal_square_iff";
-val HFinite_square_iff = thm "HFinite_square_iff";
-val HInfinite_square_iff = thm "HInfinite_square_iff";
-val approx_HFinite_mult_cancel = thm "approx_HFinite_mult_cancel";
-val approx_HFinite_mult_cancel_iff1 = thm "approx_HFinite_mult_cancel_iff1";
-val approx_hrabs_disj = thm "approx_hrabs_disj";
-val monad_hrabs_Un_subset = thm "monad_hrabs_Un_subset";
-val Infinitesimal_monad_eq = thm "Infinitesimal_monad_eq";
-val mem_monad_iff = thm "mem_monad_iff";
-val Infinitesimal_monad_zero_iff = thm "Infinitesimal_monad_zero_iff";
-val monad_zero_minus_iff = thm "monad_zero_minus_iff";
-val monad_zero_hrabs_iff = thm "monad_zero_hrabs_iff";
-val mem_monad_self = thm "mem_monad_self";
-val approx_subset_monad = thm "approx_subset_monad";
-val approx_subset_monad2 = thm "approx_subset_monad2";
-val mem_monad_approx = thm "mem_monad_approx";
-val approx_mem_monad = thm "approx_mem_monad";
-val approx_mem_monad2 = thm "approx_mem_monad2";
-val approx_mem_monad_zero = thm "approx_mem_monad_zero";
-val Infinitesimal_approx_hrabs = thm "Infinitesimal_approx_hrabs";
-val less_Infinitesimal_less = thm "less_Infinitesimal_less";
-val Ball_mem_monad_gt_zero = thm "Ball_mem_monad_gt_zero";
-val Ball_mem_monad_less_zero = thm "Ball_mem_monad_less_zero";
-val approx_hrabs = thm "approx_hrabs";
-val approx_hrabs_zero_cancel = thm "approx_hrabs_zero_cancel";
-val approx_hrabs_add_Infinitesimal = thm "approx_hrabs_add_Infinitesimal";
-val approx_hrabs_add_minus_Infinitesimal = thm "approx_hrabs_add_minus_Infinitesimal";
-val hrabs_add_Infinitesimal_cancel = thm "hrabs_add_Infinitesimal_cancel";
-val hrabs_add_minus_Infinitesimal_cancel = thm "hrabs_add_minus_Infinitesimal_cancel";
-val Infinitesimal_add_hypreal_of_real_less = thm "Infinitesimal_add_hypreal_of_real_less";
-val Infinitesimal_add_hrabs_hypreal_of_real_less = thm "Infinitesimal_add_hrabs_hypreal_of_real_less";
-val Infinitesimal_add_hrabs_hypreal_of_real_less2 = thm "Infinitesimal_add_hrabs_hypreal_of_real_less2";
-val hypreal_of_real_le_add_Infininitesimal_cancel2 = thm"hypreal_of_real_le_add_Infininitesimal_cancel2";
-val hypreal_of_real_less_Infinitesimal_le_zero = thm "hypreal_of_real_less_Infinitesimal_le_zero";
-val Infinitesimal_add_not_zero = thm "Infinitesimal_add_not_zero";
-val Infinitesimal_square_cancel = thm "Infinitesimal_square_cancel";
-val HFinite_square_cancel = thm "HFinite_square_cancel";
-val Infinitesimal_square_cancel2 = thm "Infinitesimal_square_cancel2";
-val HFinite_square_cancel2 = thm "HFinite_square_cancel2";
-val Infinitesimal_sum_square_cancel = thm "Infinitesimal_sum_square_cancel";
-val HFinite_sum_square_cancel = thm "HFinite_sum_square_cancel";
-val Infinitesimal_sum_square_cancel2 = thm "Infinitesimal_sum_square_cancel2";
-val HFinite_sum_square_cancel2 = thm "HFinite_sum_square_cancel2";
-val Infinitesimal_sum_square_cancel3 = thm "Infinitesimal_sum_square_cancel3";
-val HFinite_sum_square_cancel3 = thm "HFinite_sum_square_cancel3";
-val monad_hrabs_less = thm "monad_hrabs_less";
-val mem_monad_SReal_HFinite = thm "mem_monad_SReal_HFinite";
-val st_approx_self = thm "st_approx_self";
-val st_SReal = thm "st_SReal";
-val st_HFinite = thm "st_HFinite";
-val st_SReal_eq = thm "st_SReal_eq";
-val st_hypreal_of_real = thm "st_hypreal_of_real";
-val st_eq_approx = thm "st_eq_approx";
-val approx_st_eq = thm "approx_st_eq";
-val st_eq_approx_iff = thm "st_eq_approx_iff";
-val st_Infinitesimal_add_SReal = thm "st_Infinitesimal_add_SReal";
-val st_Infinitesimal_add_SReal2 = thm "st_Infinitesimal_add_SReal2";
-val HFinite_st_Infinitesimal_add = thm "HFinite_st_Infinitesimal_add";
-val st_add = thm "st_add";
-val st_number_of = thm "st_number_of";
-val st_minus = thm "st_minus";
-val st_diff = thm "st_diff";
-val st_mult = thm "st_mult";
-val st_Infinitesimal = thm "st_Infinitesimal";
-val st_not_Infinitesimal = thm "st_not_Infinitesimal";
-val st_inverse = thm "st_inverse";
-val st_divide = thm "st_divide";
-val st_idempotent = thm "st_idempotent";
-val Infinitesimal_add_st_less = thm "Infinitesimal_add_st_less";
-val Infinitesimal_add_st_le_cancel = thm "Infinitesimal_add_st_le_cancel";
-val st_le = thm "st_le";
-val st_zero_le = thm "st_zero_le";
-val st_zero_ge = thm "st_zero_ge";
-val st_hrabs = thm "st_hrabs";
-val FreeUltrafilterNat_HFinite = thm "FreeUltrafilterNat_HFinite";
-val HFinite_FreeUltrafilterNat_iff = thm "HFinite_FreeUltrafilterNat_iff";
-val FreeUltrafilterNat_const_Finite = thm "FreeUltrafilterNat_const_Finite";
-val FreeUltrafilterNat_HInfinite = thm "FreeUltrafilterNat_HInfinite";
-val HInfinite_FreeUltrafilterNat_iff = thm "HInfinite_FreeUltrafilterNat_iff";
-val Infinitesimal_FreeUltrafilterNat = thm "Infinitesimal_FreeUltrafilterNat";
-val FreeUltrafilterNat_Infinitesimal = thm "FreeUltrafilterNat_Infinitesimal";
-val Infinitesimal_FreeUltrafilterNat_iff = thm "Infinitesimal_FreeUltrafilterNat_iff";
-val Infinitesimal_hypreal_of_nat_iff = thm "Infinitesimal_hypreal_of_nat_iff";
-val Suc_Un_eq = thm "Suc_Un_eq";
-val finite_nat_segment = thm "finite_nat_segment";
-val finite_real_of_nat_segment = thm "finite_real_of_nat_segment";
-val finite_real_of_nat_less_real = thm "finite_real_of_nat_less_real";
-val finite_real_of_nat_le_real = thm "finite_real_of_nat_le_real";
-val finite_rabs_real_of_nat_le_real = thm "finite_rabs_real_of_nat_le_real";
-val rabs_real_of_nat_le_real_FreeUltrafilterNat = thm "rabs_real_of_nat_le_real_FreeUltrafilterNat";
-val FreeUltrafilterNat_nat_gt_real = thm "FreeUltrafilterNat_nat_gt_real";
-val FreeUltrafilterNat_omega = thm "FreeUltrafilterNat_omega";
-val HInfinite_omega = thm "HInfinite_omega";
-val Infinitesimal_epsilon = thm "Infinitesimal_epsilon";
-val HFinite_epsilon = thm "HFinite_epsilon";
-val epsilon_approx_zero = thm "epsilon_approx_zero";
-val real_of_nat_less_inverse_iff = thm "real_of_nat_less_inverse_iff";
-val finite_inverse_real_of_posnat_gt_real = thm "finite_inverse_real_of_posnat_gt_real";
-val real_of_nat_inverse_le_iff = thm "real_of_nat_inverse_le_iff";
-val real_of_nat_inverse_eq_iff = thm "real_of_nat_inverse_eq_iff";
-val finite_inverse_real_of_posnat_ge_real = thm "finite_inverse_real_of_posnat_ge_real";
-val inverse_real_of_posnat_ge_real_FreeUltrafilterNat = thm "inverse_real_of_posnat_ge_real_FreeUltrafilterNat";
-val FreeUltrafilterNat_inverse_real_of_posnat = thm "FreeUltrafilterNat_inverse_real_of_posnat";
-val real_seq_to_hypreal_Infinitesimal = thm "real_seq_to_hypreal_Infinitesimal";
-val real_seq_to_hypreal_approx = thm "real_seq_to_hypreal_approx";
-val real_seq_to_hypreal_approx2 = thm "real_seq_to_hypreal_approx2";
-val real_seq_to_hypreal_Infinitesimal2 = thm "real_seq_to_hypreal_Infinitesimal2";
-val HInfinite_HFinite_add = thm "HInfinite_HFinite_add";
-val HInfinite_ge_HInfinite = thm "HInfinite_ge_HInfinite";
-val Infinitesimal_inverse_HInfinite = thm "Infinitesimal_inverse_HInfinite";
-val HInfinite_HFinite_not_Infinitesimal_mult = thm "HInfinite_HFinite_not_Infinitesimal_mult";
-val HInfinite_HFinite_not_Infinitesimal_mult2 = thm "HInfinite_HFinite_not_Infinitesimal_mult2";
-val HInfinite_gt_SReal = thm "HInfinite_gt_SReal";
-val HInfinite_gt_zero_gt_one = thm "HInfinite_gt_zero_gt_one";
-val not_HInfinite_one = thm "not_HInfinite_one";
-*}
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/NatStar.thy
--- a/src/HOL/Hyperreal/NatStar.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/NatStar.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -182,51 +182,12 @@
 apply (simp_all add: HNatInfinite_not_eq_zero starfunNat_real_of_nat)
 done
 
-ML
-{*
-val starset_n_Un = thm "starset_n_Un";
-val InternalSets_Un = thm "InternalSets_Un";
-val starset_n_Int = thm "starset_n_Int";
-val InternalSets_Int = thm "InternalSets_Int";
-val starset_n_Compl = thm "starset_n_Compl";
-val InternalSets_Compl = thm "InternalSets_Compl";
-val starset_n_diff = thm "starset_n_diff";
-val InternalSets_diff = thm "InternalSets_diff";
-val NatStar_SHNat_subset = thm "NatStar_SHNat_subset";
-val NatStar_hypreal_of_real_Int = thm "NatStar_hypreal_of_real_Int";
-val starset_starset_n_eq = thm "starset_starset_n_eq";
-val InternalSets_starset_n = thm "InternalSets_starset_n";
-val InternalSets_UNIV_diff = thm "InternalSets_UNIV_diff";
-val starset_n_starset = thm "starset_n_starset";
-val starfun_const_fun = thm "starfun_const_fun";
-val starfun_le_mono = thm "starfun_le_mono";
-val starfun_less_mono = thm "starfun_less_mono";
-val starfun_shift_one = thm "starfun_shift_one";
-val starfun_abs = thm "starfun_abs";
-val starfun_pow = thm "starfun_pow";
-val starfun_pow2 = thm "starfun_pow2";
-val starfun_pow3 = thm "starfun_pow3";
-val starfunNat_real_of_nat = thm "starfunNat_real_of_nat";
-val starfun_inverse_real_of_nat_eq = thm "starfun_inverse_real_of_nat_eq";
-val starfun_n = thm "starfun_n";
-val starfun_n_mult = thm "starfun_n_mult";
-val starfun_n_add = thm "starfun_n_add";
-val starfun_n_add_minus = thm "starfun_n_add_minus";
-val starfun_n_const_fun = thm "starfun_n_const_fun";
-val starfun_n_minus = thm "starfun_n_minus";
-val starfun_n_eq = thm "starfun_n_eq";
-val starfun_eq_iff = thm "starfun_eq_iff";
-val starfunNat_inverse_real_of_nat_Infinitesimal = thm "starfunNat_inverse_real_of_nat_Infinitesimal";
-*}
-
-
 
 subsection{*Nonstandard Characterization of Induction*}
 
-
-constdefs
+definition
   hSuc :: "hypnat => hypnat"
-  "hSuc n == n + 1"
+  "hSuc n = n + 1"
 
 lemma starP: "(( *p* P) (star_n X)) = ({n. P (X n)} \<in> FreeUltrafilterNat)"
 by (rule starP_star_n)
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/NthRoot.thy
--- a/src/HOL/Hyperreal/NthRoot.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/NthRoot.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -170,17 +170,4 @@
 apply (drule_tac [4] x = y in realpow_less, auto)
 done
 
-ML
-{*
-val nth_realpow_isLub_ex = thm"nth_realpow_isLub_ex";
-val realpow_nth_ge = thm"realpow_nth_ge";
-val less_isLub_not_isUb = thm"less_isLub_not_isUb";
-val not_isUb_less_ex = thm"not_isUb_less_ex";
-val realpow_nth_le = thm"realpow_nth_le";
-val realpow_nth = thm"realpow_nth";
-val realpow_pos_nth = thm"realpow_pos_nth";
-val realpow_pos_nth2 = thm"realpow_pos_nth2";
-val realpow_pos_nth_unique = thm"realpow_pos_nth_unique";
-*}
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/Poly.thy
--- a/src/HOL/Hyperreal/Poly.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/Poly.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -81,29 +81,29 @@
 
 text{*Other definitions*}
 
-constdefs
-   poly_minus :: "real list => real list"      ("-- _" [80] 80)
-   "-- p == (- 1) %* p"
+definition
+  poly_minus :: "real list => real list"      ("-- _" [80] 80)
+  "-- p = (- 1) %* p"
 
-   pderiv :: "real list => real list"
-   "pderiv p == if p = [] then [] else pderiv_aux 1 (tl p)"
+  pderiv :: "real list => real list"
+  "pderiv p = (if p = [] then [] else pderiv_aux 1 (tl p))"
 
-   divides :: "[real list,real list] => bool"  (infixl "divides" 70)
-   "p1 divides p2 == \<exists>q. poly p2 = poly(p1 *** q)"
+  divides :: "[real list,real list] => bool"  (infixl "divides" 70)
+  "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
 
-   order :: "real => real list => nat"
-     --{*order of a polynomial*}
-   "order a p == (@n. ([-a, 1] %^ n) divides p &
+  order :: "real => real list => nat"
+    --{*order of a polynomial*}
+  "order a p = (SOME n. ([-a, 1] %^ n) divides p &
                       ~ (([-a, 1] %^ (Suc n)) divides p))"
 
-   degree :: "real list => nat"
+  degree :: "real list => nat"
      --{*degree of a polynomial*}
-   "degree p == length (pnormalize p)"
+  "degree p = length (pnormalize p)"
 
-   rsquarefree :: "real list => bool"
+  rsquarefree :: "real list => bool"
      --{*squarefree polynomials --- NB with respect to real roots only.*}
-   "rsquarefree p == poly p \<noteq> poly [] &
-                     (\<forall>a. (order a p = 0) | (order a p = 1))"
+  "rsquarefree p = (poly p \<noteq> poly [] &
+                     (\<forall>a. (order a p = 0) | (order a p = 1)))"
 
 
 
@@ -1026,135 +1026,4 @@
 apply (auto intro!: mult_mono simp add: abs_mult, arith)
 done
 
-ML
-{*
-val padd_Nil2 = thm "padd_Nil2";
-val padd_Cons_Cons = thm "padd_Cons_Cons";
-val pminus_Nil = thm "pminus_Nil";
-val pmult_singleton = thm "pmult_singleton";
-val poly_ident_mult = thm "poly_ident_mult";
-val poly_simple_add_Cons = thm "poly_simple_add_Cons";
-val padd_commut = thm "padd_commut";
-val padd_assoc = thm "padd_assoc";
-val poly_cmult_distr = thm "poly_cmult_distr";
-val pmult_by_x = thm "pmult_by_x";
-val poly_add = thm "poly_add";
-val poly_cmult = thm "poly_cmult";
-val poly_minus = thm "poly_minus";
-val poly_mult = thm "poly_mult";
-val poly_exp = thm "poly_exp";
-val poly_add_rzero = thm "poly_add_rzero";
-val poly_mult_assoc = thm "poly_mult_assoc";
-val poly_mult_Nil2 = thm "poly_mult_Nil2";
-val poly_exp_add = thm "poly_exp_add";
-val pderiv_Nil = thm "pderiv_Nil";
-val pderiv_singleton = thm "pderiv_singleton";
-val pderiv_Cons = thm "pderiv_Cons";
-val DERIV_cmult2 = thm "DERIV_cmult2";
-val DERIV_pow2 = thm "DERIV_pow2";
-val lemma_DERIV_poly1 = thm "lemma_DERIV_poly1";
-val lemma_DERIV_poly = thm "lemma_DERIV_poly";
-val DERIV_add_const = thm "DERIV_add_const";
-val poly_DERIV = thm "poly_DERIV";
-val poly_differentiable = thm "poly_differentiable";
-val poly_isCont = thm "poly_isCont";
-val poly_IVT_pos = thm "poly_IVT_pos";
-val poly_IVT_neg = thm "poly_IVT_neg";
-val poly_MVT = thm "poly_MVT";
-val lemma_poly_pderiv_aux_add = thm "lemma_poly_pderiv_aux_add";
-val poly_pderiv_aux_add = thm "poly_pderiv_aux_add";
-val lemma_poly_pderiv_aux_cmult = thm "lemma_poly_pderiv_aux_cmult";
-val poly_pderiv_aux_cmult = thm "poly_pderiv_aux_cmult";
-val poly_pderiv_aux_minus = thm "poly_pderiv_aux_minus";
-val lemma_poly_pderiv_aux_mult1 = thm "lemma_poly_pderiv_aux_mult1";
-val lemma_poly_pderiv_aux_mult = thm "lemma_poly_pderiv_aux_mult";
-val lemma_poly_pderiv_add = thm "lemma_poly_pderiv_add";
-val poly_pderiv_add = thm "poly_pderiv_add";
-val poly_pderiv_cmult = thm "poly_pderiv_cmult";
-val poly_pderiv_minus = thm "poly_pderiv_minus";
-val lemma_poly_mult_pderiv = thm "lemma_poly_mult_pderiv";
-val poly_pderiv_mult = thm "poly_pderiv_mult";
-val poly_pderiv_exp = thm "poly_pderiv_exp";
-val poly_pderiv_exp_prime = thm "poly_pderiv_exp_prime";
-val lemma_poly_linear_rem = thm "lemma_poly_linear_rem";
-val poly_linear_rem = thm "poly_linear_rem";
-val poly_linear_divides = thm "poly_linear_divides";
-val lemma_poly_length_mult = thm "lemma_poly_length_mult";
-val lemma_poly_length_mult2 = thm "lemma_poly_length_mult2";
-val poly_length_mult = thm "poly_length_mult";
-val poly_cmult_length = thm "poly_cmult_length";
-val poly_add_length = thm "poly_add_length";
-val poly_root_mult_length = thm "poly_root_mult_length";
-val poly_mult_not_eq_poly_Nil = thm "poly_mult_not_eq_poly_Nil";
-val poly_mult_eq_zero_disj = thm "poly_mult_eq_zero_disj";
-val poly_normalized_nil = thm "poly_normalized_nil";
-val poly_roots_index_lemma = thm "poly_roots_index_lemma";
-val poly_roots_index_lemma2 = thms "poly_roots_index_lemma2";
-val poly_roots_index_length = thm "poly_roots_index_length";
-val poly_roots_finite_lemma = thm "poly_roots_finite_lemma";
-val real_finite_lemma = thm "real_finite_lemma";
-val poly_roots_finite = thm "poly_roots_finite";
-val poly_entire_lemma = thm "poly_entire_lemma";
-val poly_entire = thm "poly_entire";
-val poly_entire_neg = thm "poly_entire_neg";
-val fun_eq = thm "fun_eq";
-val poly_add_minus_zero_iff = thm "poly_add_minus_zero_iff";
-val poly_add_minus_mult_eq = thm "poly_add_minus_mult_eq";
-val poly_mult_left_cancel = thm "poly_mult_left_cancel";
-val real_mult_zero_disj_iff = thm "real_mult_zero_disj_iff";
-val poly_exp_eq_zero = thm "poly_exp_eq_zero";
-val poly_prime_eq_zero = thm "poly_prime_eq_zero";
-val poly_exp_prime_eq_zero = thm "poly_exp_prime_eq_zero";
-val poly_zero_lemma = thm "poly_zero_lemma";
-val poly_zero = thm "poly_zero";
-val pderiv_aux_iszero = thm "pderiv_aux_iszero";
-val pderiv_aux_iszero_num = thm "pderiv_aux_iszero_num";
-val pderiv_iszero = thm "pderiv_iszero";
-val pderiv_zero_obj = thm "pderiv_zero_obj";
-val pderiv_zero = thm "pderiv_zero";
-val poly_pderiv_welldef = thm "poly_pderiv_welldef";
-val poly_primes = thm "poly_primes";
-val poly_divides_refl = thm "poly_divides_refl";
-val poly_divides_trans = thm "poly_divides_trans";
-val poly_divides_exp = thm "poly_divides_exp";
-val poly_exp_divides = thm "poly_exp_divides";
-val poly_divides_add = thm "poly_divides_add";
-val poly_divides_diff = thm "poly_divides_diff";
-val poly_divides_diff2 = thm "poly_divides_diff2";
-val poly_divides_zero = thm "poly_divides_zero";
-val poly_divides_zero2 = thm "poly_divides_zero2";
-val poly_order_exists_lemma = thm "poly_order_exists_lemma";
-val poly_order_exists = thm "poly_order_exists";
-val poly_one_divides = thm "poly_one_divides";
-val poly_order = thm "poly_order";
-val some1_equalityD = thm "some1_equalityD";
-val order = thm "order";
-val order2 = thm "order2";
-val order_unique = thm "order_unique";
-val order_unique_lemma = thm "order_unique_lemma";
-val order_poly = thm "order_poly";
-val pexp_one = thm "pexp_one";
-val lemma_order_root = thm "lemma_order_root";
-val order_root = thm "order_root";
-val order_divides = thm "order_divides";
-val order_decomp = thm "order_decomp";
-val order_mult = thm "order_mult";
-val lemma_order_pderiv = thm "lemma_order_pderiv";
-val order_pderiv = thm "order_pderiv";
-val poly_squarefree_decomp_order = thm "poly_squarefree_decomp_order";
-val poly_squarefree_decomp_order2 = thm "poly_squarefree_decomp_order2";
-val order_root2 = thm "order_root2";
-val order_pderiv2 = thm "order_pderiv2";
-val rsquarefree_roots = thm "rsquarefree_roots";
-val pmult_one = thm "pmult_one";
-val poly_Nil_zero = thm "poly_Nil_zero";
-val rsquarefree_decomp = thm "rsquarefree_decomp";
-val poly_squarefree_decomp = thm "poly_squarefree_decomp";
-val poly_normalize = thm "poly_normalize";
-val lemma_degree_zero = thm "lemma_degree_zero";
-val degree_zero = thm "degree_zero";
-val poly_roots_finite_set = thm "poly_roots_finite_set";
-val poly_mono = thm "poly_mono";
-*}
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -12,56 +12,55 @@
 imports NatStar
 begin
 
-constdefs
+definition
 
   LIMSEQ :: "[nat=>real,real] => bool"    ("((_)/ ----> (_))" [60, 60] 60)
     --{*Standard definition of convergence of sequence*}
-  "X ----> L == (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X n + -L\<bar> < r))"
+  "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> \<bar>X n + -L\<bar> < r))"
 
   NSLIMSEQ :: "[nat=>real,real] => bool"    ("((_)/ ----NS> (_))" [60, 60] 60)
     --{*Nonstandard definition of convergence of sequence*}
-  "X ----NS> L == (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> hypreal_of_real L)"
+  "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> hypreal_of_real L)"
 
   lim :: "(nat => real) => real"
     --{*Standard definition of limit using choice operator*}
-  "lim X == (@L. (X ----> L))"
+  "lim X = (SOME L. (X ----> L))"
 
   nslim :: "(nat => real) => real"
     --{*Nonstandard definition of limit using choice operator*}
-  "nslim X == (@L. (X ----NS> L))"
+  "nslim X = (SOME L. (X ----NS> L))"
 
   convergent :: "(nat => real) => bool"
     --{*Standard definition of convergence*}
-  "convergent X == (\<exists>L. (X ----> L))"
+  "convergent X = (\<exists>L. (X ----> L))"
 
   NSconvergent :: "(nat => real) => bool"
     --{*Nonstandard definition of convergence*}
-  "NSconvergent X == (\<exists>L. (X ----NS> L))"
+  "NSconvergent X = (\<exists>L. (X ----NS> L))"
 
   Bseq :: "(nat => real) => bool"
     --{*Standard definition for bounded sequence*}
-  "Bseq X == \<exists>K>0.\<forall>n. \<bar>X n\<bar> \<le> K"
+  "Bseq X = (\<exists>K>0.\<forall>n. \<bar>X n\<bar> \<le> K)"
 
   NSBseq :: "(nat=>real) => bool"
     --{*Nonstandard definition for bounded sequence*}
-  "NSBseq X == (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
+  "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
 
   monoseq :: "(nat=>real)=>bool"
     --{*Definition for monotonicity*}
-  "monoseq X == (\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m)"
+  "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
 
   subseq :: "(nat => nat) => bool"
     --{*Definition of subsequence*}
-  "subseq f == \<forall>m. \<forall>n>m. (f m) < (f n)"
+  "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
 
   Cauchy :: "(nat => real) => bool"
     --{*Standard definition of the Cauchy condition*}
-  "Cauchy X == \<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. abs((X m) + -(X n)) < e"
+  "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. abs((X m) + -(X n)) < e)"
 
   NSCauchy :: "(nat => real) => bool"
     --{*Nonstandard definition*}
-  "NSCauchy X == (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite.
-                      ( *f* X) M \<approx> ( *f* X) N)"
+  "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
 
 
 
@@ -1195,125 +1194,4 @@
 Goal "subseq f ==> \<exists>n. N1 \<le> n & N2 \<le> f(n)";
  ---------------------------------------------------------------***)
 
-
-ML
-{*
-val Cauchy_def = thm"Cauchy_def";
-val SEQ_Infinitesimal = thm "SEQ_Infinitesimal";
-val LIMSEQ_iff = thm "LIMSEQ_iff";
-val NSLIMSEQ_iff = thm "NSLIMSEQ_iff";
-val LIMSEQ_NSLIMSEQ = thm "LIMSEQ_NSLIMSEQ";
-val NSLIMSEQ_finite_set = thm "NSLIMSEQ_finite_set";
-val Compl_less_set = thm "Compl_less_set";
-val FreeUltrafilterNat_NSLIMSEQ = thm "FreeUltrafilterNat_NSLIMSEQ";
-val HNatInfinite_NSLIMSEQ = thm "HNatInfinite_NSLIMSEQ";
-val NSLIMSEQ_LIMSEQ = thm "NSLIMSEQ_LIMSEQ";
-val LIMSEQ_NSLIMSEQ_iff = thm "LIMSEQ_NSLIMSEQ_iff";
-val NSLIMSEQ_const = thm "NSLIMSEQ_const";
-val LIMSEQ_const = thm "LIMSEQ_const";
-val NSLIMSEQ_add = thm "NSLIMSEQ_add";
-val LIMSEQ_add = thm "LIMSEQ_add";
-val NSLIMSEQ_mult = thm "NSLIMSEQ_mult";
-val LIMSEQ_mult = thm "LIMSEQ_mult";
-val NSLIMSEQ_minus = thm "NSLIMSEQ_minus";
-val LIMSEQ_minus = thm "LIMSEQ_minus";
-val LIMSEQ_minus_cancel = thm "LIMSEQ_minus_cancel";
-val NSLIMSEQ_minus_cancel = thm "NSLIMSEQ_minus_cancel";
-val NSLIMSEQ_add_minus = thm "NSLIMSEQ_add_minus";
-val LIMSEQ_add_minus = thm "LIMSEQ_add_minus";
-val LIMSEQ_diff = thm "LIMSEQ_diff";
-val NSLIMSEQ_diff = thm "NSLIMSEQ_diff";
-val NSLIMSEQ_inverse = thm "NSLIMSEQ_inverse";
-val LIMSEQ_inverse = thm "LIMSEQ_inverse";
-val NSLIMSEQ_mult_inverse = thm "NSLIMSEQ_mult_inverse";
-val LIMSEQ_divide = thm "LIMSEQ_divide";
-val NSLIMSEQ_unique = thm "NSLIMSEQ_unique";
-val LIMSEQ_unique = thm "LIMSEQ_unique";
-val limI = thm "limI";
-val nslimI = thm "nslimI";
-val lim_nslim_iff = thm "lim_nslim_iff";
-val convergentD = thm "convergentD";
-val convergentI = thm "convergentI";
-val NSconvergentD = thm "NSconvergentD";
-val NSconvergentI = thm "NSconvergentI";
-val convergent_NSconvergent_iff = thm "convergent_NSconvergent_iff";
-val NSconvergent_NSLIMSEQ_iff = thm "NSconvergent_NSLIMSEQ_iff";
-val convergent_LIMSEQ_iff = thm "convergent_LIMSEQ_iff";
-val subseq_Suc_iff = thm "subseq_Suc_iff";
-val monoseq_Suc = thm "monoseq_Suc";
-val monoI1 = thm "monoI1";
-val monoI2 = thm "monoI2";
-val mono_SucI1 = thm "mono_SucI1";
-val mono_SucI2 = thm "mono_SucI2";
-val BseqD = thm "BseqD";
-val BseqI = thm "BseqI";
-val Bseq_iff = thm "Bseq_iff";
-val Bseq_iff1a = thm "Bseq_iff1a";
-val NSBseqD = thm "NSBseqD";
-val NSBseqI = thm "NSBseqI";
-val Bseq_NSBseq = thm "Bseq_NSBseq";
-val real_seq_to_hypreal_HInfinite = thm "real_seq_to_hypreal_HInfinite";
-val HNatInfinite_skolem_f = thm "HNatInfinite_skolem_f";
-val NSBseq_Bseq = thm "NSBseq_Bseq";
-val Bseq_NSBseq_iff = thm "Bseq_NSBseq_iff";
-val NSconvergent_NSBseq = thm "NSconvergent_NSBseq";
-val convergent_Bseq = thm "convergent_Bseq";
-val Bseq_isUb = thm "Bseq_isUb";
-val Bseq_isLub = thm "Bseq_isLub";
-val NSBseq_isUb = thm "NSBseq_isUb";
-val NSBseq_isLub = thm "NSBseq_isLub";
-val Bmonoseq_LIMSEQ = thm "Bmonoseq_LIMSEQ";
-val Bmonoseq_NSLIMSEQ = thm "Bmonoseq_NSLIMSEQ";
-val Bseq_mono_convergent = thm "Bseq_mono_convergent";
-val NSBseq_mono_NSconvergent = thm "NSBseq_mono_NSconvergent";
-val convergent_minus_iff = thm "convergent_minus_iff";
-val Bseq_minus_iff = thm "Bseq_minus_iff";
-val Bseq_monoseq_convergent = thm "Bseq_monoseq_convergent";
-val Bseq_iff2 = thm "Bseq_iff2";
-val Bseq_iff3 = thm "Bseq_iff3";
-val BseqI2 = thm "BseqI2";
-val Cauchy_NSCauchy = thm "Cauchy_NSCauchy";
-val NSCauchy_Cauchy = thm "NSCauchy_Cauchy";
-val NSCauchy_Cauchy_iff = thm "NSCauchy_Cauchy_iff";
-val less_Suc_cancel_iff = thm "less_Suc_cancel_iff";
-val SUP_rabs_subseq = thm "SUP_rabs_subseq";
-val Cauchy_Bseq = thm "Cauchy_Bseq";
-val NSCauchy_NSBseq = thm "NSCauchy_NSBseq";
-val NSCauchy_NSconvergent_iff = thm "NSCauchy_NSconvergent_iff";
-val Cauchy_convergent_iff = thm "Cauchy_convergent_iff";
-val NSLIMSEQ_le = thm "NSLIMSEQ_le";
-val LIMSEQ_le = thm "LIMSEQ_le";
-val LIMSEQ_le_const = thm "LIMSEQ_le_const";
-val NSLIMSEQ_le_const = thm "NSLIMSEQ_le_const";
-val LIMSEQ_le_const2 = thm "LIMSEQ_le_const2";
-val NSLIMSEQ_le_const2 = thm "NSLIMSEQ_le_const2";
-val NSLIMSEQ_Suc = thm "NSLIMSEQ_Suc";
-val LIMSEQ_Suc = thm "LIMSEQ_Suc";
-val NSLIMSEQ_imp_Suc = thm "NSLIMSEQ_imp_Suc";
-val LIMSEQ_imp_Suc = thm "LIMSEQ_imp_Suc";
-val LIMSEQ_Suc_iff = thm "LIMSEQ_Suc_iff";
-val NSLIMSEQ_Suc_iff = thm "NSLIMSEQ_Suc_iff";
-val LIMSEQ_rabs_zero = thm "LIMSEQ_rabs_zero";
-val NSLIMSEQ_rabs_zero = thm "NSLIMSEQ_rabs_zero";
-val NSLIMSEQ_imp_rabs = thm "NSLIMSEQ_imp_rabs";
-val LIMSEQ_imp_rabs = thm "LIMSEQ_imp_rabs";
-val LIMSEQ_inverse_zero = thm "LIMSEQ_inverse_zero";
-val NSLIMSEQ_inverse_zero = thm "NSLIMSEQ_inverse_zero";
-val LIMSEQ_inverse_real_of_nat = thm "LIMSEQ_inverse_real_of_nat";
-val NSLIMSEQ_inverse_real_of_nat = thm "NSLIMSEQ_inverse_real_of_nat";
-val LIMSEQ_inverse_real_of_nat_add = thm "LIMSEQ_inverse_real_of_nat_add";
-val NSLIMSEQ_inverse_real_of_nat_add = thm "NSLIMSEQ_inverse_real_of_nat_add";
-val LIMSEQ_inverse_real_of_nat_add_minus = thm "LIMSEQ_inverse_real_of_nat_add_minus";
-val NSLIMSEQ_inverse_real_of_nat_add_minus = thm "NSLIMSEQ_inverse_real_of_nat_add_minus";
-val LIMSEQ_inverse_real_of_nat_add_minus_mult = thm "LIMSEQ_inverse_real_of_nat_add_minus_mult";
-val NSLIMSEQ_inverse_real_of_nat_add_minus_mult = thm "NSLIMSEQ_inverse_real_of_nat_add_minus_mult";
-val NSLIMSEQ_pow = thm "NSLIMSEQ_pow";
-val LIMSEQ_pow = thm "LIMSEQ_pow";
-val Bseq_realpow = thm "Bseq_realpow";
-val monoseq_realpow = thm "monoseq_realpow";
-val convergent_realpow = thm "convergent_realpow";
-val NSLIMSEQ_realpow_zero = thm "NSLIMSEQ_realpow_zero";
-*}
-
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/Series.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -16,15 +16,15 @@
 declare atLeastLessThan_iff[iff]
 declare setsum_op_ivl_Suc[simp]
 
-constdefs
+definition
    sums  :: "(nat => real) => real => bool"     (infixr "sums" 80)
-   "f sums s  == (%n. setsum f {0..<n}) ----> s"
+   "f sums s = (%n. setsum f {0..<n}) ----> s"
 
    summable :: "(nat=>real) => bool"
-   "summable f == (\<exists>s. f sums s)"
+   "summable f = (\<exists>s. f sums s)"
 
    suminf   :: "(nat=>real) => real"
-   "suminf f == SOME s. f sums s"
+   "suminf f = (SOME s. f sums s)"
 
 syntax
   "_suminf" :: "idt => real => real"    ("\<Sum>_. _" [0, 10] 10)
@@ -500,48 +500,4 @@
 apply (auto intro: DERIV_add)
 done
 
-ML
-{*
-val sums_def = thm"sums_def";
-val summable_def = thm"summable_def";
-val suminf_def = thm"suminf_def";
-
-val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero";
-val sumr_one_lb_realpow_zero = thm "sumr_one_lb_realpow_zero";
-val sumr_group = thm "sumr_group";
-val sums_summable = thm "sums_summable";
-val summable_sums = thm "summable_sums";
-val summable_sumr_LIMSEQ_suminf = thm "summable_sumr_LIMSEQ_suminf";
-val sums_unique = thm "sums_unique";
-val series_zero = thm "series_zero";
-val sums_mult = thm "sums_mult";
-val sums_divide = thm "sums_divide";
-val sums_diff = thm "sums_diff";
-val suminf_mult = thm "suminf_mult";
-val suminf_mult2 = thm "suminf_mult2";
-val suminf_diff = thm "suminf_diff";
-val sums_minus = thm "sums_minus";
-val sums_group = thm "sums_group";
-val sumr_pos_lt_pair_lemma = thm "sumr_pos_lt_pair_lemma";
-val sumr_pos_lt_pair = thm "sumr_pos_lt_pair";
-val series_pos_le = thm "series_pos_le";
-val series_pos_less = thm "series_pos_less";
-val sumr_geometric = thm "sumr_geometric";
-val geometric_sums = thm "geometric_sums";
-val summable_convergent_sumr_iff = thm "summable_convergent_sumr_iff";
-val summable_Cauchy = thm "summable_Cauchy";
-val summable_comparison_test = thm "summable_comparison_test";
-val summable_rabs_comparison_test = thm "summable_rabs_comparison_test";
-val summable_le = thm "summable_le";
-val summable_le2 = thm "summable_le2";
-val summable_rabs_cancel = thm "summable_rabs_cancel";
-val summable_rabs = thm "summable_rabs";
-val rabs_ratiotest_lemma = thm "rabs_ratiotest_lemma";
-val le_Suc_ex = thm "le_Suc_ex";
-val le_Suc_ex_iff = thm "le_Suc_ex_iff";
-val ratio_test_lemma2 = thm "ratio_test_lemma2";
-val ratio_test = thm "ratio_test";
-val DERIV_sumr = thm "DERIV_sumr";
-*}
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/Star.thy
--- a/src/HOL/Hyperreal/Star.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/Star.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -10,26 +10,24 @@
 imports NSA
 begin
 
-constdefs
+definition
     (* internal sets *)
-    starset_n :: "(nat => 'a set) => 'a star set"        ("*sn* _" [80] 80)
-    "*sn* As == Iset (star_n As)"
+  starset_n :: "(nat => 'a set) => 'a star set"        ("*sn* _" [80] 80)
+  "*sn* As = Iset (star_n As)"
 
-    InternalSets :: "'a star set set"
-    "InternalSets == {X. \<exists>As. X = *sn* As}"
+  InternalSets :: "'a star set set"
+  "InternalSets = {X. \<exists>As. X = *sn* As}"
 
-    (* nonstandard extension of function *)
-    is_starext  :: "['a star => 'a star, 'a => 'a] => bool"
-    "is_starext F f == (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
+  (* nonstandard extension of function *)
+  is_starext  :: "['a star => 'a star, 'a => 'a] => bool"
+  "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
                         ((y = (F x)) = ({n. Y n = f(X n)} : FreeUltrafilterNat)))"
-    (* internal functions *)
-    starfun_n :: "(nat => ('a => 'b)) => 'a star => 'b star"
-                 ("*fn* _" [80] 80)
-    "*fn* F == Ifun (star_n F)"
+  (* internal functions *)
+  starfun_n :: "(nat => ('a => 'b)) => 'a star => 'b star"   ("*fn* _" [80] 80)
+  "*fn* F = Ifun (star_n F)"
 
-    InternalFuns :: "('a star => 'b star) set"
-    "InternalFuns == {X. \<exists>F. X = *fn* F}"
-
+  InternalFuns :: "('a star => 'b star) set"
+  "InternalFuns = {X. \<exists>F. X = *fn* F}"
 
 
 (*--------------------------------------------------------
@@ -353,66 +351,4 @@
 apply (auto simp add: starfun star_n_eq_iff)
 done
 
-ML
-{*
-val starset_n_def = thm"starset_n_def";
-val InternalSets_def = thm"InternalSets_def";
-val is_starext_def = thm"is_starext_def";
-val starfun_n_def = thm"starfun_n_def";
-val InternalFuns_def = thm"InternalFuns_def";
-
-val no_choice = thm "no_choice";
-val STAR_UNIV_set = thm "STAR_UNIV_set";
-val STAR_empty_set = thm "STAR_empty_set";
-val STAR_Un = thm "STAR_Un";
-val STAR_Int = thm "STAR_Int";
-val STAR_Compl = thm "STAR_Compl";
-val STAR_mem_Compl = thm "STAR_mem_Compl";
-val STAR_diff = thm "STAR_diff";
-val STAR_subset = thm "STAR_subset";
-val STAR_mem = thm "STAR_mem";
-val STAR_star_of_image_subset = thm "STAR_star_of_image_subset";
-val STAR_hypreal_of_real_Int = thm "STAR_hypreal_of_real_Int";
-val STAR_real_seq_to_hypreal = thm "STAR_real_seq_to_hypreal";
-val STAR_singleton = thm "STAR_singleton";
-val STAR_not_mem = thm "STAR_not_mem";
-val STAR_subset_closed = thm "STAR_subset_closed";
-val starset_n_starset = thm "starset_n_starset";
-val starfun_n_starfun = thm "starfun_n_starfun";
-val hrabs_is_starext_rabs = thm "hrabs_is_starext_rabs";
-val Rep_star_FreeUltrafilterNat = thm "Rep_star_FreeUltrafilterNat";
-val starfun = thm "starfun";
-val starfun_mult = thm "starfun_mult";
-val starfun_add = thm "starfun_add";
-val starfun_minus = thm "starfun_minus";
-val starfun_add_minus = thm "starfun_add_minus";
-val starfun_diff = thm "starfun_diff";
-val starfun_o2 = thm "starfun_o2";
-val starfun_o = thm "starfun_o";
-val starfun_const_fun = thm "starfun_const_fun";
-val starfun_Idfun_approx = thm "starfun_Idfun_approx";
-val starfun_Id = thm "starfun_Id";
-val is_starext_starfun = thm "is_starext_starfun";
-val is_starfun_starext = thm "is_starfun_starext";
-val is_starext_starfun_iff = thm "is_starext_starfun_iff";
-val starfun_eq = thm "starfun_eq";
-val starfun_approx = thm "starfun_approx";
-val starfun_lambda_cancel = thm "starfun_lambda_cancel";
-val starfun_lambda_cancel2 = thm "starfun_lambda_cancel2";
-val starfun_mult_HFinite_approx = thm "starfun_mult_HFinite_approx";
-val starfun_add_approx = thm "starfun_add_approx";
-val starfun_rabs_hrabs = thm "starfun_rabs_hrabs";
-val starfun_inverse_inverse = thm "starfun_inverse_inverse";
-val starfun_inverse = thm "starfun_inverse";
-val starfun_divide = thm "starfun_divide";
-val starfun_inverse2 = thm "starfun_inverse2";
-val starfun_mem_starset = thm "starfun_mem_starset";
-val hypreal_hrabs = thm "hypreal_hrabs";
-val STAR_rabs_add_minus = thm "STAR_rabs_add_minus";
-val STAR_starfun_rabs_add_minus = thm "STAR_starfun_rabs_add_minus";
-val Infinitesimal_FreeUltrafilterNat_iff2 = thm "Infinitesimal_FreeUltrafilterNat_iff2";
-val approx_FreeUltrafilterNat_iff = thm "approx_FreeUltrafilterNat_iff";
-val inj_starfun = thm "inj_starfun";
-*}
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/StarDef.thy
--- a/src/HOL/Hyperreal/StarDef.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/StarDef.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -12,19 +12,19 @@
 
 subsection {* A Free Ultrafilter over the Naturals *}
 
-constdefs
+definition
   FreeUltrafilterNat :: "nat set set"  ("\<U>")
-    "\<U> \<equiv> SOME U. freeultrafilter U"
+  "\<U> = (SOME U. freeultrafilter U)"
 
 lemma freeultrafilter_FUFNat: "freeultrafilter \<U>"
  apply (unfold FreeUltrafilterNat_def)
  apply (rule someI_ex)
  apply (rule freeultrafilter_Ex)
  apply (rule nat_infinite)
-done
+ done
 
 interpretation FUFNat: freeultrafilter [FreeUltrafilterNat]
-by (cut_tac [!] freeultrafilter_FUFNat, simp_all add: freeultrafilter_def)
+  using freeultrafilter_FUFNat by (simp_all add: freeultrafilter_def)
 
 text {* This rule takes the place of the old ultra tactic *}
 
@@ -35,16 +35,16 @@
 
 subsection {* Definition of @{text star} type constructor *}
 
-constdefs
+definition
   starrel :: "((nat \<Rightarrow> 'a) \<times> (nat \<Rightarrow> 'a)) set"
-    "starrel \<equiv> {(X,Y). {n. X n = Y n} \<in> \<U>}"
+  "starrel = {(X,Y). {n. X n = Y n} \<in> \<U>}"
 
 typedef 'a star = "(UNIV :: (nat \<Rightarrow> 'a) set) // starrel"
 by (auto intro: quotientI)
 
-constdefs
+definition
   star_n :: "(nat \<Rightarrow> 'a) \<Rightarrow> 'a star"
-  "star_n X \<equiv> Abs_star (starrel `` {X})"
+  "star_n X = Abs_star (starrel `` {X})"
 
 theorem star_cases [case_names star_n, cases type: star]:
   "(\<And>X. x = star_n X \<Longrightarrow> P) \<Longrightarrow> P"
@@ -156,9 +156,9 @@
 
 subsection {* Standard elements *}
 
-constdefs
+definition
   star_of :: "'a \<Rightarrow> 'a star"
-  "star_of x \<equiv> star_n (\<lambda>n. x)"
+  "star_of x == star_n (\<lambda>n. x)"
 
 text {* Transfer tactic should remove occurrences of @{term star_of} *}
 setup {* Transfer.add_const "StarDef.star_of" *}
@@ -170,7 +170,7 @@
 
 subsection {* Internal functions *}
 
-constdefs
+definition
   Ifun :: "('a \<Rightarrow> 'b) star \<Rightarrow> 'a star \<Rightarrow> 'b star" ("_ \<star> _" [300,301] 300)
   "Ifun f \<equiv> \<lambda>x. Abs_star
        (\<Union>F\<in>Rep_star f. \<Union>X\<in>Rep_star x. starrel``{\<lambda>n. F n (X n)})"
@@ -195,14 +195,14 @@
 
 text {* Nonstandard extensions of functions *}
 
-constdefs
+definition
   starfun :: "('a \<Rightarrow> 'b) \<Rightarrow> ('a star \<Rightarrow> 'b star)"
     ("*f* _" [80] 80)
-  "starfun f \<equiv> \<lambda>x. star_of f \<star> x"
+  "starfun f == \<lambda>x. star_of f \<star> x"
 
   starfun2 :: "('a \<Rightarrow> 'b \<Rightarrow> 'c) \<Rightarrow> ('a star \<Rightarrow> 'b star \<Rightarrow> 'c star)"
     ("*f2* _" [80] 80)
-  "starfun2 f \<equiv> \<lambda>x y. star_of f \<star> x \<star> y"
+  "starfun2 f == \<lambda>x y. star_of f \<star> x \<star> y"
 
 declare starfun_def [transfer_unfold]
 declare starfun2_def [transfer_unfold]
@@ -223,9 +223,9 @@
 
 subsection {* Internal predicates *}
 
-constdefs
+definition
   unstar :: "bool star \<Rightarrow> bool"
-  "unstar b \<equiv> b = star_of True"
+  "unstar b = (b = star_of True)"
 
 lemma unstar_star_n: "unstar (star_n P) = ({n. P n} \<in> \<U>)"
 by (simp add: unstar_def star_of_def star_n_eq_iff)
@@ -240,14 +240,14 @@
   "p \<equiv> star_n P \<Longrightarrow> unstar p \<equiv> {n. P n} \<in> \<U>"
 by (simp only: unstar_star_n)
 
-constdefs
+definition
   starP :: "('a \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> bool"
     ("*p* _" [80] 80)
-  "*p* P \<equiv> \<lambda>x. unstar (star_of P \<star> x)"
+  "*p* P = (\<lambda>x. unstar (star_of P \<star> x))"
 
   starP2 :: "('a \<Rightarrow> 'b \<Rightarrow> bool) \<Rightarrow> 'a star \<Rightarrow> 'b star \<Rightarrow> bool"
     ("*p2* _" [80] 80)
-  "*p2* P \<equiv> \<lambda>x y. unstar (star_of P \<star> x \<star> y)"
+  "*p2* P = (\<lambda>x y. unstar (star_of P \<star> x \<star> y))"
 
 declare starP_def [transfer_unfold]
 declare starP2_def [transfer_unfold]
@@ -268,9 +268,9 @@
 
 subsection {* Internal sets *}
 
-constdefs
+definition
   Iset :: "'a set star \<Rightarrow> 'a star set"
-  "Iset A \<equiv> {x. ( *p2* op \<in>) x A}"
+  "Iset A = {x. ( *p2* op \<in>) x A}"
 
 lemma Iset_star_n:
   "(star_n X \<in> Iset (star_n A)) = ({n. X n \<in> A n} \<in> \<U>)"
@@ -309,9 +309,10 @@
 by simp
 
 text {* Nonstandard extensions of sets. *}
-constdefs
+
+definition
   starset :: "'a set \<Rightarrow> 'a star set" ("*s* _" [80] 80)
-  "starset A \<equiv> Iset (star_of A)"
+  "starset A = Iset (star_of A)"
 
 declare starset_def [transfer_unfold]
 
diff -r 372065f34795 -r dfe940911617 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -11,44 +11,44 @@
 imports NthRoot Fact HSeries EvenOdd Lim
 begin
 
-constdefs
-    root :: "[nat,real] => real"
-    "root n x == (@u. ((0::real) < x --> 0 < u) & (u ^ n = x))"
-
-    sqrt :: "real => real"
-    "sqrt x == root 2 x"
-
-    exp :: "real => real"
-    "exp x == \<Sum>n. inverse(real (fact n)) * (x ^ n)"
-
-    sin :: "real => real"
-    "sin x == \<Sum>n. (if even(n) then 0 else
-             ((- 1) ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n"
+definition
+  root :: "[nat,real] => real"
+  "root n x = (SOME u. ((0::real) < x --> 0 < u) & (u ^ n = x))"
+
+  sqrt :: "real => real"
+  "sqrt x = root 2 x"
+
+  exp :: "real => real"
+  "exp x = (\<Sum>n. inverse(real (fact n)) * (x ^ n))"
+
+  sin :: "real => real"
+  "sin x = (\<Sum>n. (if even(n) then 0 else
+             ((- 1) ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)"
  
-    diffs :: "(nat => real) => nat => real"
-    "diffs c == (%n. real (Suc n) * c(Suc n))"
-
-    cos :: "real => real"
-    "cos x == \<Sum>n. (if even(n) then ((- 1) ^ (n div 2))/(real (fact n)) 
-                          else 0) * x ^ n"
+  diffs :: "(nat => real) => nat => real"
+  "diffs c = (%n. real (Suc n) * c(Suc n))"
+
+  cos :: "real => real"
+  "cos x = (\<Sum>n. (if even(n) then ((- 1) ^ (n div 2))/(real (fact n)) 
+                            else 0) * x ^ n)"
   
-    ln :: "real => real"
-    "ln x == (@u. exp u = x)"
-
-    pi :: "real"
-    "pi == 2 * (@x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
-
-    tan :: "real => real"
-    "tan x == (sin x)/(cos x)"
-
-    arcsin :: "real => real"
-    "arcsin y == (@x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
-
-    arcos :: "real => real"
-    "arcos y == (@x. 0 \<le> x & x \<le> pi & cos x = y)"
+  ln :: "real => real"
+  "ln x = (SOME u. exp u = x)"
+
+  pi :: "real"
+  "pi = 2 * (@x. 0 \<le> (x::real) & x \<le> 2 & cos x = 0)"
+
+  tan :: "real => real"
+  "tan x = (sin x)/(cos x)"
+
+  arcsin :: "real => real"
+  "arcsin y = (SOME x. -(pi/2) \<le> x & x \<le> pi/2 & sin x = y)"
+
+  arcos :: "real => real"
+  "arcos y = (SOME x. 0 \<le> x & x \<le> pi & cos x = y)"
      
-    arctan :: "real => real"
-    "arctan y == (@x. -(pi/2) < x & x < pi/2 & tan x = y)"
+  arctan :: "real => real"
+  "arctan y = (SOME x. -(pi/2) < x & x < pi/2 & tan x = y)"
 
 
 lemma real_root_zero [simp]: "root (Suc n) 0 = 0"
@@ -2578,298 +2578,5 @@
 apply (drule_tac [3] LIM_fun_gt_zero)
 apply force+
 done
-
-ML
-{*
-val inverse_unique = thm "inverse_unique";
-val real_root_zero = thm "real_root_zero";
-val real_root_pow_pos = thm "real_root_pow_pos";
-val real_root_pow_pos2 = thm "real_root_pow_pos2";
-val real_root_pos = thm "real_root_pos";
-val real_root_pos2 = thm "real_root_pos2";
-val real_root_pos_pos = thm "real_root_pos_pos";
-val real_root_pos_pos_le = thm "real_root_pos_pos_le";
-val real_root_one = thm "real_root_one";
-val root_2_eq = thm "root_2_eq";
-val real_sqrt_zero = thm "real_sqrt_zero";
-val real_sqrt_one = thm "real_sqrt_one";
-val real_sqrt_pow2_iff = thm "real_sqrt_pow2_iff";
-val real_sqrt_pow2 = thm "real_sqrt_pow2";
-val real_sqrt_abs_abs = thm "real_sqrt_abs_abs";
-val real_pow_sqrt_eq_sqrt_pow = thm "real_pow_sqrt_eq_sqrt_pow";
-val real_pow_sqrt_eq_sqrt_abs_pow2 = thm "real_pow_sqrt_eq_sqrt_abs_pow2";
-val real_sqrt_pow_abs = thm "real_sqrt_pow_abs";
-val not_real_square_gt_zero = thm "not_real_square_gt_zero";
-val real_sqrt_gt_zero = thm "real_sqrt_gt_zero";
-val real_sqrt_ge_zero = thm "real_sqrt_ge_zero";
-val sqrt_eqI = thm "sqrt_eqI";
-val real_sqrt_mult_distrib = thm "real_sqrt_mult_distrib";
-val real_sqrt_mult_distrib2 = thm "real_sqrt_mult_distrib2";
-val real_sqrt_sum_squares_ge_zero = thm "real_sqrt_sum_squares_ge_zero";
-val real_sqrt_sum_squares_mult_ge_zero = thm "real_sqrt_sum_squares_mult_ge_zero";
-val real_sqrt_sum_squares_mult_squared_eq = thm "real_sqrt_sum_squares_mult_squared_eq";
-val real_sqrt_abs = thm "real_sqrt_abs";
-val real_sqrt_abs2 = thm "real_sqrt_abs2";
-val real_sqrt_pow2_gt_zero = thm "real_sqrt_pow2_gt_zero";
-val real_sqrt_not_eq_zero = thm "real_sqrt_not_eq_zero";
-val real_inv_sqrt_pow2 = thm "real_inv_sqrt_pow2";
-val real_sqrt_eq_zero_cancel = thm "real_sqrt_eq_zero_cancel";
-val real_sqrt_eq_zero_cancel_iff = thm "real_sqrt_eq_zero_cancel_iff";
-val real_sqrt_sum_squares_ge1 = thm "real_sqrt_sum_squares_ge1";
-val real_sqrt_sum_squares_ge2 = thm "real_sqrt_sum_squares_ge2";
-val real_sqrt_ge_one = thm "real_sqrt_ge_one";
-val summable_exp = thm "summable_exp";
-val summable_sin = thm "summable_sin";
-val summable_cos = thm "summable_cos";
-val exp_converges = thm "exp_converges";
-val sin_converges = thm "sin_converges";
-val cos_converges = thm "cos_converges";
-val powser_insidea = thm "powser_insidea";
-val powser_inside = thm "powser_inside";
-val diffs_minus = thm "diffs_minus";
-val diffs_equiv = thm "diffs_equiv";
-val less_add_one = thm "less_add_one";
-val termdiffs_aux = thm "termdiffs_aux";
-val termdiffs = thm "termdiffs";
-val exp_fdiffs = thm "exp_fdiffs";
-val sin_fdiffs = thm "sin_fdiffs";
-val sin_fdiffs2 = thm "sin_fdiffs2";
-val cos_fdiffs = thm "cos_fdiffs";
-val cos_fdiffs2 = thm "cos_fdiffs2";
-val DERIV_exp = thm "DERIV_exp";
-val DERIV_sin = thm "DERIV_sin";
-val DERIV_cos = thm "DERIV_cos";
-val exp_zero = thm "exp_zero";
-(* val exp_ge_add_one_self = thm "exp_ge_add_one_self"; *)
-val exp_gt_one = thm "exp_gt_one";
-val DERIV_exp_add_const = thm "DERIV_exp_add_const";
-val DERIV_exp_minus = thm "DERIV_exp_minus";
-val DERIV_exp_exp_zero = thm "DERIV_exp_exp_zero";
-val exp_add_mult_minus = thm "exp_add_mult_minus";
-val exp_mult_minus = thm "exp_mult_minus";
-val exp_mult_minus2 = thm "exp_mult_minus2";
-val exp_minus = thm "exp_minus";
-val exp_add = thm "exp_add";
-val exp_ge_zero = thm "exp_ge_zero";
-val exp_not_eq_zero = thm "exp_not_eq_zero";
-val exp_gt_zero = thm "exp_gt_zero";
-val inv_exp_gt_zero = thm "inv_exp_gt_zero";
-val abs_exp_cancel = thm "abs_exp_cancel";
-val exp_real_of_nat_mult = thm "exp_real_of_nat_mult";
-val exp_diff = thm "exp_diff";
-val exp_less_mono = thm "exp_less_mono";
-val exp_less_cancel = thm "exp_less_cancel";
-val exp_less_cancel_iff = thm "exp_less_cancel_iff";
-val exp_le_cancel_iff = thm "exp_le_cancel_iff";
-val exp_inj_iff = thm "exp_inj_iff";
-val exp_total = thm "exp_total";
-val ln_exp = thm "ln_exp";
-val exp_ln_iff = thm "exp_ln_iff";
-val ln_mult = thm "ln_mult";
-val ln_inj_iff = thm "ln_inj_iff";
-val ln_one = thm "ln_one";
-val ln_inverse = thm "ln_inverse";
-val ln_div = thm "ln_div";
-val ln_less_cancel_iff = thm "ln_less_cancel_iff";
-val ln_le_cancel_iff = thm "ln_le_cancel_iff";
-val ln_realpow = thm "ln_realpow";
-val ln_add_one_self_le_self = thm "ln_add_one_self_le_self";
-val ln_less_self = thm "ln_less_self";
-val ln_ge_zero = thm "ln_ge_zero";
-val ln_gt_zero = thm "ln_gt_zero";
-val ln_less_zero = thm "ln_less_zero";
-val exp_ln_eq = thm "exp_ln_eq";
-val sin_zero = thm "sin_zero";
-val cos_zero = thm "cos_zero";
-val DERIV_sin_sin_mult = thm "DERIV_sin_sin_mult";
-val DERIV_sin_sin_mult2 = thm "DERIV_sin_sin_mult2";
-val DERIV_sin_realpow2 = thm "DERIV_sin_realpow2";
-val DERIV_sin_realpow2a = thm "DERIV_sin_realpow2a";
-val DERIV_cos_cos_mult = thm "DERIV_cos_cos_mult";
-val DERIV_cos_cos_mult2 = thm "DERIV_cos_cos_mult2";
-val DERIV_cos_realpow2 = thm "DERIV_cos_realpow2";
-val DERIV_cos_realpow2a = thm "DERIV_cos_realpow2a";
-val DERIV_cos_realpow2b = thm "DERIV_cos_realpow2b";
-val DERIV_cos_cos_mult3 = thm "DERIV_cos_cos_mult3";
-val DERIV_sin_circle_all = thm "DERIV_sin_circle_all";
-val DERIV_sin_circle_all_zero = thm "DERIV_sin_circle_all_zero";
-val sin_cos_squared_add = thm "sin_cos_squared_add";
-val sin_cos_squared_add2 = thm "sin_cos_squared_add2";
-val sin_cos_squared_add3 = thm "sin_cos_squared_add3";
-val sin_squared_eq = thm "sin_squared_eq";
-val cos_squared_eq = thm "cos_squared_eq";
-val real_gt_one_ge_zero_add_less = thm "real_gt_one_ge_zero_add_less";
-val abs_sin_le_one = thm "abs_sin_le_one";
-val sin_ge_minus_one = thm "sin_ge_minus_one";
-val sin_le_one = thm "sin_le_one";
-val abs_cos_le_one = thm "abs_cos_le_one";
-val cos_ge_minus_one = thm "cos_ge_minus_one";
-val cos_le_one = thm "cos_le_one";
-val DERIV_fun_pow = thm "DERIV_fun_pow";
-val DERIV_fun_exp = thm "DERIV_fun_exp";
-val DERIV_fun_sin = thm "DERIV_fun_sin";
-val DERIV_fun_cos = thm "DERIV_fun_cos";
-val DERIV_intros = thms "DERIV_intros";
-val sin_cos_add = thm "sin_cos_add";
-val sin_add = thm "sin_add";
-val cos_add = thm "cos_add";
-val sin_cos_minus = thm "sin_cos_minus";
-val sin_minus = thm "sin_minus";
-val cos_minus = thm "cos_minus";
-val sin_diff = thm "sin_diff";
-val sin_diff2 = thm "sin_diff2";
-val cos_diff = thm "cos_diff";
-val cos_diff2 = thm "cos_diff2";
-val sin_double = thm "sin_double";
-val cos_double = thm "cos_double";
-val sin_paired = thm "sin_paired";
-val sin_gt_zero = thm "sin_gt_zero";
-val sin_gt_zero1 = thm "sin_gt_zero1";
-val cos_double_less_one = thm "cos_double_less_one";
-val cos_paired = thm "cos_paired";
-val cos_two_less_zero = thm "cos_two_less_zero";
-val cos_is_zero = thm "cos_is_zero";
-val pi_half = thm "pi_half";
-val cos_pi_half = thm "cos_pi_half";
-val pi_half_gt_zero = thm "pi_half_gt_zero";
-val pi_half_less_two = thm "pi_half_less_two";
-val pi_gt_zero = thm "pi_gt_zero";
-val pi_neq_zero = thm "pi_neq_zero";
-val pi_not_less_zero = thm "pi_not_less_zero";
-val pi_ge_zero = thm "pi_ge_zero";
-val minus_pi_half_less_zero = thm "minus_pi_half_less_zero";
-val sin_pi_half = thm "sin_pi_half";
-val cos_pi = thm "cos_pi";
-val sin_pi = thm "sin_pi";
-val sin_cos_eq = thm "sin_cos_eq";
-val minus_sin_cos_eq = thm "minus_sin_cos_eq";
-val cos_sin_eq = thm "cos_sin_eq";
-val sin_periodic_pi = thm "sin_periodic_pi";
-val sin_periodic_pi2 = thm "sin_periodic_pi2";
-val cos_periodic_pi = thm "cos_periodic_pi";
-val sin_periodic = thm "sin_periodic";
-val cos_periodic = thm "cos_periodic";
-val cos_npi = thm "cos_npi";
-val sin_npi = thm "sin_npi";
-val sin_npi2 = thm "sin_npi2";
-val cos_two_pi = thm "cos_two_pi";
-val sin_two_pi = thm "sin_two_pi";
-val sin_gt_zero2 = thm "sin_gt_zero2";
-val sin_less_zero = thm "sin_less_zero";
-val pi_less_4 = thm "pi_less_4";
-val cos_gt_zero = thm "cos_gt_zero";
-val cos_gt_zero_pi = thm "cos_gt_zero_pi";
-val cos_ge_zero = thm "cos_ge_zero";
-val sin_gt_zero_pi = thm "sin_gt_zero_pi";
-val sin_ge_zero = thm "sin_ge_zero";
-val cos_total = thm "cos_total";
-val sin_total = thm "sin_total";
-val reals_Archimedean4 = thm "reals_Archimedean4";
-val cos_zero_lemma = thm "cos_zero_lemma";
-val sin_zero_lemma = thm "sin_zero_lemma";
-val cos_zero_iff = thm "cos_zero_iff";
-val sin_zero_iff = thm "sin_zero_iff";
-val tan_zero = thm "tan_zero";
-val tan_pi = thm "tan_pi";
-val tan_npi = thm "tan_npi";
-val tan_minus = thm "tan_minus";
-val tan_periodic = thm "tan_periodic";
-val add_tan_eq = thm "add_tan_eq";
-val tan_add = thm "tan_add";
-val tan_double = thm "tan_double";
-val tan_gt_zero = thm "tan_gt_zero";
-val tan_less_zero = thm "tan_less_zero";
-val DERIV_tan = thm "DERIV_tan";
-val LIM_cos_div_sin = thm "LIM_cos_div_sin";
-val tan_total_pos = thm "tan_total_pos";
-val tan_total = thm "tan_total";
-val arcsin_pi = thm "arcsin_pi";
-val arcsin = thm "arcsin";
-val sin_arcsin = thm "sin_arcsin";
-val arcsin_bounded = thm "arcsin_bounded";
-val arcsin_lbound = thm "arcsin_lbound";
-val arcsin_ubound = thm "arcsin_ubound";
-val arcsin_lt_bounded = thm "arcsin_lt_bounded";
-val arcsin_sin = thm "arcsin_sin";
-val arcos = thm "arcos";
-val cos_arcos = thm "cos_arcos";
-val arcos_bounded = thm "arcos_bounded";
-val arcos_lbound = thm "arcos_lbound";
-val arcos_ubound = thm "arcos_ubound";
-val arcos_lt_bounded = thm "arcos_lt_bounded";
-val arcos_cos = thm "arcos_cos";
-val arcos_cos2 = thm "arcos_cos2";
-val arctan = thm "arctan";
-val tan_arctan = thm "tan_arctan";
-val arctan_bounded = thm "arctan_bounded";
-val arctan_lbound = thm "arctan_lbound";
-val arctan_ubound = thm "arctan_ubound";
-val arctan_tan = thm "arctan_tan";
-val arctan_zero_zero = thm "arctan_zero_zero";
-val cos_arctan_not_zero = thm "cos_arctan_not_zero";
-val tan_sec = thm "tan_sec";
-val DERIV_sin_add = thm "DERIV_sin_add";
-val cos_2npi = thm "cos_2npi";
-val cos_3over2_pi = thm "cos_3over2_pi";
-val sin_2npi = thm "sin_2npi";
-val sin_3over2_pi = thm "sin_3over2_pi";
-val cos_pi_eq_zero = thm "cos_pi_eq_zero";
-val DERIV_cos_add = thm "DERIV_cos_add";
-val isCont_cos = thm "isCont_cos";
-val isCont_sin = thm "isCont_sin";
-val isCont_exp = thm "isCont_exp";
-val sin_zero_abs_cos_one = thm "sin_zero_abs_cos_one";
-val exp_eq_one_iff = thm "exp_eq_one_iff";
-val cos_one_sin_zero = thm "cos_one_sin_zero";
-val real_root_less_mono = thm "real_root_less_mono";
-val real_root_le_mono = thm "real_root_le_mono";
-val real_root_less_iff = thm "real_root_less_iff";
-val real_root_le_iff = thm "real_root_le_iff";
-val real_root_eq_iff = thm "real_root_eq_iff";
-val real_root_pos_unique = thm "real_root_pos_unique";
-val real_root_mult = thm "real_root_mult";
-val real_root_inverse = thm "real_root_inverse";
-val real_root_divide = thm "real_root_divide";
-val real_sqrt_less_mono = thm "real_sqrt_less_mono";
-val real_sqrt_le_mono = thm "real_sqrt_le_mono";
-val real_sqrt_less_iff = thm "real_sqrt_less_iff";
-val real_sqrt_le_iff = thm "real_sqrt_le_iff";
-val real_sqrt_eq_iff = thm "real_sqrt_eq_iff";
-val real_sqrt_sos_less_one_iff = thm "real_sqrt_sos_less_one_iff";
-val real_sqrt_sos_eq_one_iff = thm "real_sqrt_sos_eq_one_iff";
-val real_divide_square_eq = thm "real_divide_square_eq";
-val real_sqrt_sum_squares_gt_zero1 = thm "real_sqrt_sum_squares_gt_zero1";
-val real_sqrt_sum_squares_gt_zero2 = thm "real_sqrt_sum_squares_gt_zero2";
-val real_sqrt_sum_squares_gt_zero3 = thm "real_sqrt_sum_squares_gt_zero3";
-val real_sqrt_sum_squares_gt_zero3a = thm "real_sqrt_sum_squares_gt_zero3a";
-val cos_x_y_ge_minus_one = thm "cos_x_y_ge_minus_one";
-val cos_x_y_ge_minus_one1a = thm "cos_x_y_ge_minus_one1a";
-val cos_x_y_le_one = thm "cos_x_y_le_one";
-val cos_x_y_le_one2 = thm "cos_x_y_le_one2";
-val cos_abs_x_y_ge_minus_one = thm "cos_abs_x_y_ge_minus_one";
-val cos_abs_x_y_le_one = thm "cos_abs_x_y_le_one";
-val minus_pi_less_zero = thm "minus_pi_less_zero";
-val arcos_ge_minus_pi = thm "arcos_ge_minus_pi";
-val sin_x_y_disj = thm "sin_x_y_disj";
-val cos_x_y_disj = thm "cos_x_y_disj";
-val real_sqrt_divide_less_zero = thm "real_sqrt_divide_less_zero";
-val polar_ex1 = thm "polar_ex1";
-val polar_ex2 = thm "polar_ex2";
-val polar_Ex = thm "polar_Ex";
-val real_sqrt_ge_abs1 = thm "real_sqrt_ge_abs1";
-val real_sqrt_ge_abs2 = thm "real_sqrt_ge_abs2";
-val real_sqrt_two_gt_zero = thm "real_sqrt_two_gt_zero";
-val real_sqrt_two_ge_zero = thm "real_sqrt_two_ge_zero";
-val real_sqrt_two_gt_one = thm "real_sqrt_two_gt_one";
-val STAR_exp_ln = thm "STAR_exp_ln";
-val hypreal_add_Infinitesimal_gt_zero = thm "hypreal_add_Infinitesimal_gt_zero";
-val NSDERIV_exp_ln_one = thm "NSDERIV_exp_ln_one";
-val DERIV_exp_ln_one = thm "DERIV_exp_ln_one";
-val isCont_inv_fun = thm "isCont_inv_fun";
-val isCont_inv_fun_inv = thm "isCont_inv_fun_inv";
-val LIM_fun_gt_zero = thm "LIM_fun_gt_zero";
-val LIM_fun_less_zero = thm "LIM_fun_less_zero";
-val LIM_fun_not_zero = thm "LIM_fun_not_zero";
-*}
   
 end 
diff -r 372065f34795 -r dfe940911617 src/HOL/Real/ContNotDenum.thy
--- a/src/HOL/Real/ContNotDenum.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Real/ContNotDenum.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -36,8 +36,9 @@
 
 subsection {* Definition *}
 
-constdefs closed_int :: "real \<Rightarrow> real \<Rightarrow> real set"
-  "closed_int x y \<equiv> {z. x \<le> z \<and> z \<le> y}"
+definition
+  closed_int :: "real \<Rightarrow> real \<Rightarrow> real set"
+  "closed_int x y = {z. x \<le> z \<and> z \<le> y}"
 
 subsection {* Properties *}
 
@@ -48,9 +49,9 @@
   {
     fix x::real
     assume "x \<in> closed_int x1 y1"
-    hence "x \<ge> x1 \<and> x \<le> y1" by (unfold closed_int_def, simp)
+    hence "x \<ge> x1 \<and> x \<le> y1" by (simp add: closed_int_def)
     with xy have "x \<ge> x0 \<and> x \<le> y0" by auto
-    hence "x \<in> closed_int x0 y0" by (unfold closed_int_def, simp)
+    hence "x \<in> closed_int x0 y0" by (simp add: closed_int_def)
   }
   thus ?thesis by auto
 qed
@@ -575,4 +576,4 @@
   ultimately show False by blast
 qed
 
-end
\ No newline at end of file
+end
diff -r 372065f34795 -r dfe940911617 src/HOL/Real/Float.thy
--- a/src/HOL/Real/Float.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Real/Float.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -5,11 +5,11 @@
 
 theory Float imports Real begin
 
-constdefs  
+definition
   pow2 :: "int \<Rightarrow> real"
-  "pow2 a == if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a))))" 
+  "pow2 a = (if (0 <= a) then (2^(nat a)) else (inverse (2^(nat (-a)))))"
   float :: "int * int \<Rightarrow> real"
-  "float x == (real (fst x)) * (pow2 (snd x))"
+  "float x = real (fst x) * pow2 (snd x)"
 
 lemma pow2_0[simp]: "pow2 0 = 1"
 by (simp add: pow2_def)
@@ -20,7 +20,7 @@
 lemma pow2_neg: "pow2 x = inverse (pow2 (-x))"
 by (simp add: pow2_def)
 
-lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)" 
+lemma pow2_add1: "pow2 (1 + a) = 2 * (pow2 a)"
 proof -
   have h: "! n. nat (2 + int n) - Suc 0 = nat (1 + int n)" by arith
   have g: "! a b. a - -1 = a + (1::int)" by arith
@@ -30,7 +30,7 @@
     apply (rule_tac m1="2" and n1="nat (2 + int na)" in ssubst[OF realpow_num_eq_if])
     apply (auto simp add: h)
     apply arith
-    done  
+    done
   show ?thesis
   proof (induct a)
     case (1 n)
@@ -43,12 +43,12 @@
       apply (subst pow2_neg[of "-1 - int n"])
       apply (auto simp add: g pos)
       done
-  qed  
+  qed
 qed
-  
+
 lemma pow2_add: "pow2 (a+b) = (pow2 a) * (pow2 b)"
 proof (induct b)
-  case (1 n) 
+  case (1 n)
   show ?case
   proof (induct n)
     case 0
@@ -59,10 +59,10 @@
   qed
 next
   case (2 n)
-  show ?case 
+  show ?case
   proof (induct n)
     case 0
-    show ?case 
+    show ?case
       apply (auto)
       apply (subst pow2_neg[of "a + -1"])
       apply (subst pow2_neg[of "-1"])
@@ -73,7 +73,7 @@
       apply (simp)
       done
     case (Suc m)
-    have a: "int m - (a + -2) =  1 + (int m - a + 1)" by arith	
+    have a: "int m - (a + -2) =  1 + (int m - a + 1)" by arith
     have b: "int m - -2 = 1 + (int m + 1)" by arith
     show ?case
       apply (auto)
@@ -92,14 +92,14 @@
   qed
 qed
 
-lemma "float (a, e) + float (b, e) = float (a + b, e)"  
+lemma "float (a, e) + float (b, e) = float (a + b, e)"
 by (simp add: float_def ring_eq_simps)
 
-constdefs 
+definition
   int_of_real :: "real \<Rightarrow> int"
-  "int_of_real x == SOME y. real y = x"  
+  "int_of_real x = (SOME y. real y = x)"
   real_is_int :: "real \<Rightarrow> bool"
-  "real_is_int x == ? (u::int). x = real u" 
+  "real_is_int x = (EX (u::int). x = real u)"
 
 lemma real_is_int_def2: "real_is_int x = (x = real (int_of_real x))"
 by (auto simp add: real_is_int_def int_of_real_def)
@@ -110,7 +110,7 @@
 lemma pow2_int: "pow2 (int c) = (2::real)^c"
 by (simp add: pow2_def)
 
-lemma float_transfer_nat: "float (a, b) = float (a * 2^c, b - int c)" 
+lemma float_transfer_nat: "float (a, b) = float (a * 2^c, b - int c)"
 by (simp add: float_def pow2_int[symmetric] pow2_add[symmetric])
 
 lemma real_is_int_real[simp]: "real_is_int (real (x::int))"
@@ -141,7 +141,7 @@
 lemma real_is_int_rep: "real_is_int x \<Longrightarrow> ?! (a::int). real a = x"
 by (auto simp add: real_is_int_def)
 
-lemma int_of_real_mult: 
+lemma int_of_real_mult:
   assumes "real_is_int a" "real_is_int b"
   shows "(int_of_real (a*b)) = (int_of_real a) * (int_of_real b)"
 proof -
@@ -187,8 +187,8 @@
     also have "\<dots> = True" by (simp only: real_is_int_real)
     ultimately show ?thesis by auto
   qed
-  
-  { 
+
+  {
     fix x::int
     have "!! y. real_is_int ((number_of::bin\<Rightarrow>real) (Abs_Bin x))"
       apply (simp add: number_of_eq)
@@ -205,11 +205,11 @@
       assume rn: "(real_is_int (of_int (- (int (Suc n)))))"
       have s: "-(int (Suc (Suc n))) = -1 + - (int (Suc n))" by simp
       show "real_is_int (of_int (- (int (Suc (Suc n)))))"
-	apply (simp only: s of_int_add)
-	apply (rule real_is_int_add)
-	apply (simp add: neg1)
-	apply (simp only: rn)
-	done
+        apply (simp only: s of_int_add)
+        apply (rule real_is_int_add)
+        apply (simp add: neg1)
+        apply (simp only: rn)
+        done
     qed
   }
   note Abs_Bin = this
@@ -228,7 +228,7 @@
 by (simp add: int_of_real_def)
 
 lemma int_of_real_1[simp]: "int_of_real (1::real) = (1::int)"
-proof - 
+proof -
   have 1: "(1::real) = real (1::int)" by auto
   show ?thesis by (simp only: 1 int_of_real_real)
 qed
@@ -238,9 +238,9 @@
   have "real_is_int (number_of b)" by simp
   then have uu: "?! u::int. number_of b = real u" by (auto simp add: real_is_int_rep)
   then obtain u::int where u:"number_of b = real u" by auto
-  have "number_of b = real ((number_of b)::int)" 
+  have "number_of b = real ((number_of b)::int)"
     by (simp add: number_of_eq real_of_int_def)
-  have ub: "number_of b = real ((number_of b)::int)" 
+  have ub: "number_of b = real ((number_of b)::int)"
     by (simp add: number_of_eq real_of_int_def)
   from uu u ub have unb: "u = number_of b"
     by blast
@@ -255,10 +255,10 @@
 proof -
   fix q::int
   have a:"b - (-1\<Colon>int) = (1\<Colon>int) + b" by arith
-  show "(float (q, (b - (-1\<Colon>int)))) = (float (q, ((1\<Colon>int) + b)))" 
+  show "(float (q, (b - (-1\<Colon>int)))) = (float (q, ((1\<Colon>int) + b)))"
     by (simp add: a)
 qed
-    
+
 consts
   norm_float :: "int*int \<Rightarrow> int*int"
 
@@ -285,7 +285,7 @@
 apply (auto)
 done
 
-ML {* simp_depth_limit := 2 *} 
+ML {* simp_depth_limit := 2 *}
 recdef norm_float "measure (% (a,b). nat (abs a))"
   "norm_float (a,b) = (if (a \<noteq> 0) & (even a) then norm_float (a div 2, b+1) else (if a=0 then (0,0) else (a,b)))"
 (hints simp: terminating_norm_float)
@@ -294,23 +294,23 @@
 lemma norm_float: "float x = float (norm_float x)"
 proof -
   {
-    fix a b :: int 
-    have norm_float_pair: "float (a,b) = float (norm_float (a,b))" 
+    fix a b :: int
+    have norm_float_pair: "float (a,b) = float (norm_float (a,b))"
     proof (induct a b rule: norm_float.induct)
       case (1 u v)
-      show ?case 
+      show ?case
       proof cases
-	assume u: "u \<noteq> 0 \<and> even u"
-	with prems have ind: "float (u div 2, v + 1) = float (norm_float (u div 2, v + 1))" by auto
-	with u have "float (u,v) = float (u div 2, v+1)" by (simp add: float_transfer_even) 
-	then show ?thesis
-	  apply (subst norm_float.simps)
-	  apply (simp add: ind)
-	  done
+        assume u: "u \<noteq> 0 \<and> even u"
+        with prems have ind: "float (u div 2, v + 1) = float (norm_float (u div 2, v + 1))" by auto
+        with u have "float (u,v) = float (u div 2, v+1)" by (simp add: float_transfer_even)
+        then show ?thesis
+          apply (subst norm_float.simps)
+          apply (simp add: ind)
+          done
       next
-	assume "~(u \<noteq> 0 \<and> even u)"
-	then show ?thesis
-	  by (simp add: prems float_def)
+        assume "~(u \<noteq> 0 \<and> even u)"
+        then show ?thesis
+          by (simp add: prems float_def)
       qed
     qed
   }
@@ -323,16 +323,16 @@
 lemma pow2_int: "pow2 (int n) = 2^n"
   by (simp add: pow2_def)
 
-lemma float_add: 
-  "float (a1, e1) + float (a2, e2) = 
-  (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1) 
+lemma float_add:
+  "float (a1, e1) + float (a2, e2) =
+  (if e1<=e2 then float (a1+a2*2^(nat(e2-e1)), e1)
   else float (a1*2^(nat (e1-e2))+a2, e2))"
   apply (simp add: float_def ring_eq_simps)
   apply (auto simp add: pow2_int[symmetric] pow2_add[symmetric])
   done
 
 lemma float_mult:
-  "float (a1, e1) * float (a2, e2) = 
+  "float (a1, e1) * float (a2, e2) =
   (float (a1 * a2, e1 + e2))"
   by (simp add: float_def pow2_add)
 
@@ -345,7 +345,7 @@
 proof -
   {
     fix y
-    have "0 <= y \<Longrightarrow> 0 < pow2 y"    
+    have "0 <= y \<Longrightarrow> 0 < pow2 y"
       by (induct y, induct_tac n, simp_all add: pow2_add)
   }
   note helper=this
@@ -360,7 +360,7 @@
 lemma zero_le_float:
   "(0 <= float (a,b)) = (0 <= a)"
   apply (auto simp add: float_def)
-  apply (auto simp add: zero_le_mult_iff zero_less_pow2) 
+  apply (auto simp add: zero_le_mult_iff zero_less_pow2)
   apply (insert zero_less_pow2[of b])
   apply (simp_all)
   done
@@ -393,7 +393,7 @@
 
 lemma norm_0_1: "(0::_::number_ring) = Numeral0 & (1::_::number_ring) = Numeral1"
   by auto
-  
+
 lemma add_left_zero: "0 + a = (a::'a::comm_monoid_add)"
   by simp
 
@@ -451,19 +451,19 @@
 lemma not_true_eq_false: "(~ True) = False" by simp
 
 
-lemmas binarith = 
+lemmas binarith =
   Pls_0_eq Min_1_eq
-  bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0     
+  bin_pred_Pls bin_pred_Min bin_pred_1 bin_pred_0
   bin_succ_Pls bin_succ_Min bin_succ_1 bin_succ_0
   bin_add_Pls bin_add_Min bin_add_BIT_0 bin_add_BIT_10
-  bin_add_BIT_11 bin_minus_Pls bin_minus_Min bin_minus_1 
-  bin_minus_0 bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0 
+  bin_add_BIT_11 bin_minus_Pls bin_minus_Min bin_minus_1
+  bin_minus_0 bin_mult_Pls bin_mult_Min bin_mult_1 bin_mult_0
   bin_add_Pls_right bin_add_Min_right
 
 lemma int_eq_number_of_eq: "(((number_of v)::int)=(number_of w)) = iszero ((number_of (bin_add v (bin_minus w)))::int)"
   by simp
 
-lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)" 
+lemma int_iszero_number_of_Pls: "iszero (Numeral0::int)"
   by (simp only: iszero_number_of_Pls)
 
 lemma int_nonzero_number_of_Min: "~(iszero ((-1)::int))"
@@ -472,13 +472,13 @@
 lemma int_iszero_number_of_0: "iszero ((number_of (w BIT bit.B0))::int) = iszero ((number_of w)::int)"
   by simp
 
-lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)" 
+lemma int_iszero_number_of_1: "\<not> iszero ((number_of (w BIT bit.B1))::int)"
   by simp
 
 lemma int_less_number_of_eq_neg: "(((number_of x)::int) < number_of y) = neg ((number_of (bin_add x (bin_minus y)))::int)"
   by simp
 
-lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))" 
+lemma int_not_neg_number_of_Pls: "\<not> (neg (Numeral0::int))"
   by simp
 
 lemma int_neg_number_of_Min: "neg (-1::int)"
@@ -490,9 +490,9 @@
 lemma int_le_number_of_eq: "(((number_of x)::int) \<le> number_of y) = (\<not> neg ((number_of (bin_add y (bin_minus x)))::int))"
   by simp
 
-lemmas intarithrel = 
-  int_eq_number_of_eq 
-  lift_bool[OF int_iszero_number_of_Pls] nlift_bool[OF int_nonzero_number_of_Min] int_iszero_number_of_0 
+lemmas intarithrel =
+  int_eq_number_of_eq
+  lift_bool[OF int_iszero_number_of_Pls] nlift_bool[OF int_nonzero_number_of_Min] int_iszero_number_of_0
   lift_bool[OF int_iszero_number_of_1] int_less_number_of_eq_neg nlift_bool[OF int_not_neg_number_of_Pls] lift_bool[OF int_neg_number_of_Min]
   int_neg_number_of_BIT int_le_number_of_eq
 
@@ -512,8 +512,8 @@
 
 lemmas natarith = add_nat_number_of diff_nat_number_of mult_nat_number_of eq_nat_number_of less_nat_number_of
 
-lemmas powerarith = nat_number_of zpower_number_of_even 
-  zpower_number_of_odd[simplified zero_eq_Numeral0_nring one_eq_Numeral1_nring]   
+lemmas powerarith = nat_number_of zpower_number_of_even
+  zpower_number_of_odd[simplified zero_eq_Numeral0_nring one_eq_Numeral1_nring]
   zpower_Pls zpower_Min
 
 lemmas floatarith[simplified norm_0_1] = float_add float_mult float_minus float_abs zero_le_float float_pprt float_nprt
@@ -522,4 +522,3 @@
 lemmas arith = binarith intarith intarithrel natarith powerarith floatarith not_false_eq_true not_true_eq_false
 
 end
- 
diff -r 372065f34795 -r dfe940911617 src/HOL/Real/Lubs.thy
--- a/src/HOL/Real/Lubs.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Real/Lubs.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -12,25 +12,25 @@
 
 text{*Thanks to suggestions by James Margetson*}
 
-constdefs
+definition
 
   setle :: "['a set, 'a::ord] => bool"     (infixl "*<=" 70)
-    "S *<= x    == (ALL y: S. y <= x)"
+  "S *<= x = (ALL y: S. y <= x)"
 
   setge :: "['a::ord, 'a set] => bool"     (infixl "<=*" 70)
-    "x <=* S    == (ALL y: S. x <= y)"
+  "x <=* S = (ALL y: S. x <= y)"
 
   leastP      :: "['a =>bool,'a::ord] => bool"
-    "leastP P x == (P x & x <=* Collect P)"
+  "leastP P x = (P x & x <=* Collect P)"
 
   isUb        :: "['a set, 'a set, 'a::ord] => bool"
-    "isUb R S x   == S *<= x & x: R"
+  "isUb R S x = (S *<= x & x: R)"
 
   isLub       :: "['a set, 'a set, 'a::ord] => bool"
-    "isLub R S x  == leastP (isUb R S) x"
+  "isLub R S x = leastP (isUb R S) x"
 
   ubs         :: "['a set, 'a::ord set] => 'a set"
-    "ubs R S      == Collect (isUb R S)"
+  "ubs R S = Collect (isUb R S)"
 
 
 
@@ -106,35 +106,4 @@
 apply (erule leastPD2)
 done
 
-ML
-{*
-val setle_def = thm "setle_def";
-val setge_def = thm "setge_def";
-val leastP_def = thm "leastP_def";
-val isLub_def = thm "isLub_def";
-val isUb_def = thm "isUb_def";
-val ubs_def = thm "ubs_def";
-
-val setleI = thm "setleI";
-val setleD = thm "setleD";
-val setgeI = thm "setgeI";
-val setgeD = thm "setgeD";
-val leastPD1 = thm "leastPD1";
-val leastPD2 = thm "leastPD2";
-val leastPD3 = thm "leastPD3";
-val isLubD1 = thm "isLubD1";
-val isLubD1a = thm "isLubD1a";
-val isLub_isUb = thm "isLub_isUb";
-val isLubD2 = thm "isLubD2";
-val isLubD3 = thm "isLubD3";
-val isLubI1 = thm "isLubI1";
-val isLubI2 = thm "isLubI2";
-val isUbD = thm "isUbD";
-val isUbD2 = thm "isUbD2";
-val isUbD2a = thm "isUbD2a";
-val isUbI = thm "isUbI";
-val isLub_le_isUb = thm "isLub_le_isUb";
-val isLub_ubs = thm "isLub_ubs";
-*}
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Real/PReal.thy
--- a/src/HOL/Real/PReal.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Real/PReal.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -27,11 +27,11 @@
 by (auto dest: dense)
 
 
-constdefs
+definition
   cut :: "rat set => bool"
-    "cut A == {} \<subset> A &
-              A < {r. 0 < r} &
-              (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u)))"
+  "cut A = ({} \<subset> A &
+            A < {r. 0 < r} &
+            (\<forall>y \<in> A. ((\<forall>z. 0<z & z < y --> z \<in> A) & (\<exists>u \<in> A. y < u))))"
 
 
 lemma cut_of_rat: 
@@ -56,24 +56,24 @@
 
 instance preal :: "{ord, plus, minus, times, inverse}" ..
 
-constdefs
+definition
   preal_of_rat :: "rat => preal"
-     "preal_of_rat q == Abs_preal({x::rat. 0 < x & x < q})"
+  "preal_of_rat q = Abs_preal({x::rat. 0 < x & x < q})"
 
   psup       :: "preal set => preal"
-    "psup(P)   == Abs_preal(\<Union>X \<in> P. Rep_preal(X))"
+  "psup(P) = Abs_preal(\<Union>X \<in> P. Rep_preal(X))"
 
   add_set :: "[rat set,rat set] => rat set"
-    "add_set A B == {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x + y}"
+  "add_set A B = {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x + y}"
 
   diff_set :: "[rat set,rat set] => rat set"
-    "diff_set A B == {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
+  "diff_set A B = {w. \<exists>x. 0 < w & 0 < x & x \<notin> B & x + w \<in> A}"
 
   mult_set :: "[rat set,rat set] => rat set"
-    "mult_set A B == {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x * y}"
+  "mult_set A B = {w. \<exists>x \<in> A. \<exists>y \<in> B. w = x * y}"
 
   inverse_set :: "rat set => rat set"
-    "inverse_set A == {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
+  "inverse_set A = {x. \<exists>y. 0 < x & x < y & inverse y \<notin> A}"
 
 
 defs (overloaded)
@@ -163,11 +163,11 @@
  Gleason p. 122 - Remark (1)*}
 
 lemma not_in_preal_ub:
-     assumes A: "A \<in> preal"
-         and notx: "x \<notin> A"
-         and y: "y \<in> A"
-         and pos: "0 < x"
-        shows "y < x"
+  assumes A: "A \<in> preal"
+    and notx: "x \<notin> A"
+    and y: "y \<in> A"
+    and pos: "0 < x"
+  shows "y < x"
 proof (cases rule: linorder_cases)
   assume "x<y"
   with notx show ?thesis
@@ -271,11 +271,11 @@
 proof (unfold add_set_def, clarify)
   fix x::rat and y::rat
   assume A: "A \<in> preal" 
-     and B: "B \<in> preal"
-     and [simp]: "0 < z"
-     and zless: "z < x + y"
-     and x:  "x \<in> A"
-     and y:  "y \<in> B"
+    and B: "B \<in> preal"
+    and [simp]: "0 < z"
+    and zless: "z < x + y"
+    and x:  "x \<in> A"
+    and y:  "y \<in> B"
   have xpos [simp]: "0<x" by (rule preal_imp_pos [OF A x])
   have ypos [simp]: "0<y" by (rule preal_imp_pos [OF B y])
   have xypos [simp]: "0 < x+y" by (simp add: pos_add_strict)
@@ -394,16 +394,15 @@
 qed
 
 lemma mult_set_not_rat_set:
-   assumes A: "A \<in> preal" 
-       and B: "B \<in> preal"
-     shows "mult_set A B < {r. 0 < r}"
+  assumes A: "A \<in> preal" 
+    and B: "B \<in> preal"
+  shows "mult_set A B < {r. 0 < r}"
 proof
   show "mult_set A B \<subseteq> {r. 0 < r}"
     by (force simp add: mult_set_def
-              intro: preal_imp_pos [OF A] preal_imp_pos [OF B] mult_pos_pos)
-next
+      intro: preal_imp_pos [OF A] preal_imp_pos [OF B] mult_pos_pos)
   show "mult_set A B \<noteq> {r. 0 < r}"
-    by (insert preal_not_mem_mult_set_Ex [OF A B], blast)
+    using preal_not_mem_mult_set_Ex [OF A B] by blast
 qed
 
 
@@ -415,11 +414,11 @@
 proof (unfold mult_set_def, clarify)
   fix x::rat and y::rat
   assume A: "A \<in> preal" 
-     and B: "B \<in> preal"
-     and [simp]: "0 < z"
-     and zless: "z < x * y"
-     and x:  "x \<in> A"
-     and y:  "y \<in> B"
+    and B: "B \<in> preal"
+    and [simp]: "0 < z"
+    and zless: "z < x * y"
+    and x:  "x \<in> A"
+    and y:  "y \<in> B"
   have [simp]: "0<y" by (rule preal_imp_pos [OF B y])
   show "\<exists>x' \<in> A. \<exists>y' \<in> B. z = x' * y'"
   proof
@@ -560,10 +559,10 @@
 
 lemma preal_add_mult_distrib_mean:
   assumes a: "a \<in> Rep_preal w"
-      and b: "b \<in> Rep_preal w"
-      and d: "d \<in> Rep_preal x"
-      and e: "e \<in> Rep_preal y"
-     shows "\<exists>c \<in> Rep_preal w. a * d + b * e = c * (d + e)"
+    and b: "b \<in> Rep_preal w"
+    and d: "d \<in> Rep_preal x"
+    and e: "e \<in> Rep_preal y"
+  shows "\<exists>c \<in> Rep_preal w. a * d + b * e = c * (d + e)"
 proof
   let ?c = "(a*d + b*e)/(d+e)"
   have [simp]: "0<a" "0<b" "0<d" "0<e" "0<d+e"
@@ -690,9 +689,9 @@
 
 lemma Gleason9_34_exists:
   assumes A: "A \<in> preal"
-      and "\<forall>x\<in>A. x + u \<in> A"
-      and "0 \<le> z"
-     shows "\<exists>b\<in>A. b + (of_int z) * u \<in> A"
+    and "\<forall>x\<in>A. x + u \<in> A"
+    and "0 \<le> z"
+  shows "\<exists>b\<in>A. b + (of_int z) * u \<in> A"
 proof (cases z rule: int_cases)
   case (nonneg n)
   show ?thesis
@@ -717,11 +716,11 @@
   fix a::int and b::int
   fix c::int and d::int
   assume bpos [simp]: "0 < b"
-     and dpos [simp]: "0 < d"
-     and closed: "\<forall>x\<in>A. x + (Fract c d) \<in> A"
-     and upos: "0 < Fract c d"
-     and ypos: "0 < Fract a b"
-     and notin: "Fract a b \<notin> A"
+    and dpos [simp]: "0 < d"
+    and closed: "\<forall>x\<in>A. x + (Fract c d) \<in> A"
+    and upos: "0 < Fract c d"
+    and ypos: "0 < Fract a b"
+    and notin: "Fract a b \<notin> A"
   have cpos [simp]: "0 < c" 
     by (simp add: zero_less_Fract_iff [OF dpos, symmetric] upos) 
   have apos [simp]: "0 < a" 
@@ -752,8 +751,8 @@
 
 lemma Gleason9_34:
   assumes A: "A \<in> preal"
-      and upos: "0 < u"
-    shows "\<exists>r \<in> A. r + u \<notin> A"
+    and upos: "0 < u"
+  shows "\<exists>r \<in> A. r + u \<notin> A"
 proof (rule ccontr, simp)
   assume closed: "\<forall>r\<in>A. r + u \<in> A"
   from preal_exists_bound [OF A]
@@ -768,8 +767,8 @@
 
 lemma lemma_gleason9_36:
   assumes A: "A \<in> preal"
-      and x: "1 < x"
-    shows "\<exists>r \<in> A. r*x \<notin> A"
+    and x: "1 < x"
+  shows "\<exists>r \<in> A. r*x \<notin> A"
 proof -
   from preal_nonempty [OF A]
   obtain y where y: "y \<in> A" and  ypos: "0<y" ..
@@ -824,9 +823,9 @@
 by (simp add: preal_of_rat_def rat_mem_preal) 
 
 lemma subset_inverse_mult_lemma:
-      assumes xpos: "0 < x" and xless: "x < 1"
-         shows "\<exists>r u y. 0 < r & r < y & inverse y \<notin> Rep_preal R & 
-                        u \<in> Rep_preal R & x = r * u"
+  assumes xpos: "0 < x" and xless: "x < 1"
+  shows "\<exists>r u y. 0 < r & r < y & inverse y \<notin> Rep_preal R & 
+    u \<in> Rep_preal R & x = r * u"
 proof -
   from xpos and xless have "1 < inverse x" by (simp add: one_less_inverse_iff)
   from lemma_gleason9_36 [OF Rep_preal this]
@@ -858,11 +857,11 @@
 done
 
 lemma inverse_mult_subset_lemma:
-     assumes rpos: "0 < r" 
-         and rless: "r < y"
-         and notin: "inverse y \<notin> Rep_preal R"
-         and q: "q \<in> Rep_preal R"
-     shows "r*q < 1"
+  assumes rpos: "0 < r" 
+    and rless: "r < y"
+    and notin: "inverse y \<notin> Rep_preal R"
+    and q: "q \<in> Rep_preal R"
+  shows "r*q < 1"
 proof -
   have "q < inverse y" using rpos rless
     by (simp add: not_in_preal_ub [OF Rep_preal notin] q)
@@ -961,7 +960,7 @@
 done
 
 lemma diff_set_not_rat_set:
-     "diff_set (Rep_preal S) (Rep_preal R) < {r. 0 < r}" (is "?lhs < ?rhs")
+  "diff_set (Rep_preal S) (Rep_preal R) < {r. 0 < r}" (is "?lhs < ?rhs")
 proof
   show "?lhs \<subseteq> ?rhs" by (auto simp add: diff_set_def) 
   show "?lhs \<noteq> ?rhs" using diff_set_nonempty by blast
@@ -1007,11 +1006,11 @@
 
 lemma less_add_left_lemma:
   assumes Rless: "R < S"
-      and a: "a \<in> Rep_preal R"
-      and cb: "c + b \<in> Rep_preal S"
-      and "c \<notin> Rep_preal R"
-      and "0 < b"
-      and "0 < c"
+    and a: "a \<in> Rep_preal R"
+    and cb: "c + b \<in> Rep_preal S"
+    and "c \<notin> Rep_preal R"
+    and "0 < b"
+    and "0 < c"
   shows "a + b \<in> Rep_preal S"
 proof -
   have "0<a" by (rule preal_imp_pos [OF Rep_preal a])
@@ -1039,8 +1038,8 @@
 
 lemma less_add_left_lemma2:
   assumes Rless: "R < S"
-      and x:     "x \<in> Rep_preal S"
-      and xnot: "x \<notin>  Rep_preal R"
+    and x:     "x \<in> Rep_preal S"
+    and xnot: "x \<notin>  Rep_preal R"
   shows "\<exists>u v z. 0 < v & 0 < z & u \<in> Rep_preal R & z \<notin> Rep_preal R & 
                      z + v \<in> Rep_preal S & x = u + v"
 proof -
@@ -1216,9 +1215,9 @@
 
 lemma preal_of_rat_add_lemma2:
   assumes "u < x + y"
-      and "0 < x"
-      and "0 < y"
-      and "0 < u"
+    and "0 < x"
+    and "0 < y"
+    and "0 < u"
   shows "\<exists>v w::rat. w < y & 0 < v & v < x & 0 < w & u = v + w"
 proof (intro exI conjI)
   show "u * x * inverse(x+y) < x" using prems 
@@ -1253,8 +1252,8 @@
 
 lemma preal_of_rat_mult_lemma2: 
   assumes xless: "x < y * z"
-      and xpos: "0 < x"
-      and ypos: "0 < y"
+    and xpos: "0 < x"
+    and ypos: "0 < y"
   shows "x * z * inverse y * inverse z < (z::rat)"
 proof -
   have "0 < y * z" using prems by simp
@@ -1270,9 +1269,9 @@
 
 lemma preal_of_rat_mult_lemma3:
   assumes uless: "u < x * y"
-      and "0 < x"
-      and "0 < y"
-      and "0 < u"
+    and "0 < x"
+    and "0 < y"
+    and "0 < u"
   shows "\<exists>v w::rat. v < x & w < y & 0 < v & 0 < w & u = v * w"
 proof -
   from dense [OF uless] 
@@ -1317,37 +1316,4 @@
       "[| 0 < x; 0 < y|] ==> (preal_of_rat x = preal_of_rat y) = (x = y)"
 by (simp add: preal_of_rat_le_iff order_eq_iff) 
 
-
-ML
-{*
-val mem_Rep_preal_Ex = thm"mem_Rep_preal_Ex";
-val preal_add_commute = thm"preal_add_commute";
-val preal_add_assoc = thm"preal_add_assoc";
-val preal_add_left_commute = thm"preal_add_left_commute";
-val preal_mult_commute = thm"preal_mult_commute";
-val preal_mult_assoc = thm"preal_mult_assoc";
-val preal_mult_left_commute = thm"preal_mult_left_commute";
-val preal_add_mult_distrib2 = thm"preal_add_mult_distrib2";
-val preal_add_mult_distrib = thm"preal_add_mult_distrib";
-val preal_self_less_add_left = thm"preal_self_less_add_left";
-val preal_self_less_add_right = thm"preal_self_less_add_right";
-val less_add_left = thm"less_add_left";
-val preal_add_less2_mono1 = thm"preal_add_less2_mono1";
-val preal_add_less2_mono2 = thm"preal_add_less2_mono2";
-val preal_add_right_less_cancel = thm"preal_add_right_less_cancel";
-val preal_add_left_less_cancel = thm"preal_add_left_less_cancel";
-val preal_add_right_cancel = thm"preal_add_right_cancel";
-val preal_add_left_cancel = thm"preal_add_left_cancel";
-val preal_add_left_cancel_iff = thm"preal_add_left_cancel_iff";
-val preal_add_right_cancel_iff = thm"preal_add_right_cancel_iff";
-val preal_psup_le = thm"preal_psup_le";
-val psup_le_ub = thm"psup_le_ub";
-val preal_complete = thm"preal_complete";
-val preal_of_rat_add = thm"preal_of_rat_add";
-val preal_of_rat_mult = thm"preal_of_rat_mult";
-
-val preal_add_ac = thms"preal_add_ac";
-val preal_mult_ac = thms"preal_mult_ac";
-*}
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Real/RComplete.thy
--- a/src/HOL/Real/RComplete.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Real/RComplete.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -429,36 +429,22 @@
 done
 
 
-ML
-{*
-val real_sum_of_halves = thm "real_sum_of_halves";
-val posreal_complete = thm "posreal_complete";
-val real_isLub_unique = thm "real_isLub_unique";
-val posreals_complete = thm "posreals_complete";
-val reals_complete = thm "reals_complete";
-val reals_Archimedean = thm "reals_Archimedean";
-val reals_Archimedean2 = thm "reals_Archimedean2";
-val reals_Archimedean3 = thm "reals_Archimedean3";
-*}
-
-
 subsection{*Floor and Ceiling Functions from the Reals to the Integers*}
 
-constdefs
-
+definition
   floor :: "real => int"
-   "floor r == (LEAST n::int. r < real (n+1))"
+  "floor r = (LEAST n::int. r < real (n+1))"
 
   ceiling :: "real => int"
-    "ceiling r == - floor (- r)"
+  "ceiling r = - floor (- r)"
 
-syntax (xsymbols)
-  floor :: "real => int"     ("\<lfloor>_\<rfloor>")
-  ceiling :: "real => int"   ("\<lceil>_\<rceil>")
+const_syntax (xsymbols)
+  floor  ("\<lfloor>_\<rfloor>")
+  ceiling  ("\<lceil>_\<rceil>")
 
-syntax (HTML output)
-  floor :: "real => int"     ("\<lfloor>_\<rfloor>")
-  ceiling :: "real => int"   ("\<lceil>_\<rceil>")
+const_syntax (HTML output)
+  floor  ("\<lfloor>_\<rfloor>")
+  ceiling  ("\<lceil>_\<rceil>")
 
 
 lemma number_of_less_real_of_int_iff [simp]:
@@ -946,11 +932,11 @@
 
 subsection {* Versions for the natural numbers *}
 
-constdefs
+definition
   natfloor :: "real => nat"
-  "natfloor x == nat(floor x)"
+  "natfloor x = nat(floor x)"
   natceiling :: "real => nat"
-  "natceiling x == nat(ceiling x)"
+  "natceiling x = nat(ceiling x)"
 
 lemma natfloor_zero [simp]: "natfloor 0 = 0"
   by (unfold natfloor_def, simp)
@@ -1300,55 +1286,4 @@
     by simp
 qed
 
-ML
-{*
-val number_of_less_real_of_int_iff = thm "number_of_less_real_of_int_iff";
-val number_of_less_real_of_int_iff2 = thm "number_of_less_real_of_int_iff2";
-val number_of_le_real_of_int_iff = thm "number_of_le_real_of_int_iff";
-val number_of_le_real_of_int_iff2 = thm "number_of_le_real_of_int_iff2";
-val floor_zero = thm "floor_zero";
-val floor_real_of_nat_zero = thm "floor_real_of_nat_zero";
-val floor_real_of_nat = thm "floor_real_of_nat";
-val floor_minus_real_of_nat = thm "floor_minus_real_of_nat";
-val floor_real_of_int = thm "floor_real_of_int";
-val floor_minus_real_of_int = thm "floor_minus_real_of_int";
-val reals_Archimedean6 = thm "reals_Archimedean6";
-val reals_Archimedean6a = thm "reals_Archimedean6a";
-val reals_Archimedean_6b_int = thm "reals_Archimedean_6b_int";
-val reals_Archimedean_6c_int = thm "reals_Archimedean_6c_int";
-val real_lb_ub_int = thm "real_lb_ub_int";
-val lemma_floor = thm "lemma_floor";
-val real_of_int_floor_le = thm "real_of_int_floor_le";
-(*val floor_le = thm "floor_le";
-val floor_le2 = thm "floor_le2";
-*)
-val lemma_floor2 = thm "lemma_floor2";
-val real_of_int_floor_cancel = thm "real_of_int_floor_cancel";
-val floor_eq = thm "floor_eq";
-val floor_eq2 = thm "floor_eq2";
-val floor_eq3 = thm "floor_eq3";
-val floor_eq4 = thm "floor_eq4";
-val floor_number_of_eq = thm "floor_number_of_eq";
-val real_of_int_floor_ge_diff_one = thm "real_of_int_floor_ge_diff_one";
-val real_of_int_floor_add_one_ge = thm "real_of_int_floor_add_one_ge";
-val ceiling_zero = thm "ceiling_zero";
-val ceiling_real_of_nat = thm "ceiling_real_of_nat";
-val ceiling_real_of_nat_zero = thm "ceiling_real_of_nat_zero";
-val ceiling_floor = thm "ceiling_floor";
-val floor_ceiling = thm "floor_ceiling";
-val real_of_int_ceiling_ge = thm "real_of_int_ceiling_ge";
-(*
-val ceiling_le = thm "ceiling_le";
-val ceiling_le2 = thm "ceiling_le2";
-*)
-val real_of_int_ceiling_cancel = thm "real_of_int_ceiling_cancel";
-val ceiling_eq = thm "ceiling_eq";
-val ceiling_eq2 = thm "ceiling_eq2";
-val ceiling_eq3 = thm "ceiling_eq3";
-val ceiling_real_of_int = thm "ceiling_real_of_int";
-val ceiling_number_of_eq = thm "ceiling_number_of_eq";
-val real_of_int_ceiling_diff_one_le = thm "real_of_int_ceiling_diff_one_le";
-val real_of_int_ceiling_le_add_one = thm "real_of_int_ceiling_le_add_one";
-*}
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Real/Rational.thy
--- a/src/HOL/Real/Rational.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Real/Rational.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -14,12 +14,12 @@
 
 subsubsection {* Equivalence of fractions *}
 
-constdefs
+definition
   fraction :: "(int \<times> int) set"
-   "fraction \<equiv> {x. snd x \<noteq> 0}"
+  "fraction = {x. snd x \<noteq> 0}"
 
   ratrel :: "((int \<times> int) \<times> (int \<times> int)) set"
-   "ratrel \<equiv> {(x,y). snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x}"
+  "ratrel = {(x,y). snd x \<noteq> 0 \<and> snd y \<noteq> 0 \<and> fst x * snd y = fst y * snd x}"
 
 lemma fraction_iff [simp]: "(x \<in> fraction) = (snd x \<noteq> 0)"
 by (simp add: fraction_def)
@@ -78,9 +78,9 @@
 declare Abs_Rat_inject [simp]  Abs_Rat_inverse [simp]
 
 
-constdefs
+definition
   Fract :: "int \<Rightarrow> int \<Rightarrow> rat"
-  "Fract a b \<equiv> Abs_Rat (ratrel``{(a,b)})"
+  "Fract a b = Abs_Rat (ratrel``{(a,b)})"
 
 theorem Rat_cases [case_names Fract, cases type: rat]:
   "(!!a b. q = Fract a b ==> b \<noteq> 0 ==> C) ==> C"
@@ -455,12 +455,9 @@
     --{*the type constraint is essential!*}
 
 instance rat :: number_ring
-by (intro_classes, simp add: rat_number_of_def) 
-
-declare diff_rat_def [symmetric]
+  by default (simp add: rat_number_of_def) 
 
 use "rat_arith.ML"
-
 setup rat_arith_setup
 
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Real/RealDef.thy
--- a/src/HOL/Real/RealDef.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Real/RealDef.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -13,22 +13,21 @@
 uses ("real_arith.ML")
 begin
 
-constdefs
+definition
   realrel   ::  "((preal * preal) * (preal * preal)) set"
-  "realrel == {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
+  "realrel = {p. \<exists>x1 y1 x2 y2. p = ((x1,y1),(x2,y2)) & x1+y2 = x2+y1}"
 
 typedef (Real)  real = "UNIV//realrel"
   by (auto simp add: quotient_def)
 
 instance real :: "{ord, zero, one, plus, times, minus, inverse}" ..
 
-constdefs
+definition
 
   (** these don't use the overloaded "real" function: users don't see them **)
 
   real_of_preal :: "preal => real"
-  "real_of_preal m     ==
-           Abs_Real(realrel``{(m + preal_of_rat 1, preal_of_rat 1)})"
+  "real_of_preal m = Abs_Real(realrel``{(m + preal_of_rat 1, preal_of_rat 1)})"
 
 consts
    (*Overloaded constant denoting the Real subset of enclosing
@@ -38,8 +37,8 @@
    (*overloaded constant for injecting other types into "real"*)
    real :: "'a => real"
 
-syntax (xsymbols)
-  Reals     :: "'a set"                   ("\<real>")
+const_syntax (xsymbols)
+  Reals  ("\<real>")
 
 
 defs (overloaded)
@@ -1018,7 +1017,6 @@
 lemma abs_le_interval_iff: "(abs x \<le> r) = (-r\<le>x & x\<le>(r::real))"
 by (force simp add: OrderedGroup.abs_le_iff)
 
-(*FIXME: used only once, in SEQ.ML*)
 lemma abs_add_one_gt_zero [simp]: "(0::real) < 1 + abs(x)"
 by (simp add: abs_if)
 
@@ -1030,7 +1028,6 @@
 apply (auto intro: abs_ge_self [THEN order_trans])
 done
  
-text{*Used only in Hyperreal/Lim.ML*}
 lemma abs_sum_triangle_ineq: "abs ((x::real) + y + (-l + -m)) \<le> abs(x + -l) + abs(y + -m)"
 apply (simp add: real_add_assoc)
 apply (rule_tac a1 = y in add_left_commute [THEN ssubst])
@@ -1038,19 +1035,4 @@
 apply (rule abs_triangle_ineq)
 done
 
-
-ML
-{*
-val real_lbound_gt_zero = thm"real_lbound_gt_zero";
-val real_less_half_sum = thm"real_less_half_sum";
-val real_gt_half_sum = thm"real_gt_half_sum";
-
-val abs_interval_iff = thm"abs_interval_iff";
-val abs_le_interval_iff = thm"abs_le_interval_iff";
-val abs_add_one_gt_zero = thm"abs_add_one_gt_zero";
-val abs_add_one_not_less_self = thm"abs_add_one_not_less_self";
-val abs_sum_triangle_ineq = thm"abs_sum_triangle_ineq";
-*}
-
-
 end
diff -r 372065f34795 -r dfe940911617 src/HOL/Real/RealPow.thy
--- a/src/HOL/Real/RealPow.thy	Fri Jun 02 20:12:59 2006 +0200
+++ b/src/HOL/Real/RealPow.thy	Fri Jun 02 23:22:29 2006 +0200
@@ -37,8 +37,7 @@
 lemma realpow_two: "(r::real)^ (Suc (Suc 0)) = r * r"
 by simp
 
-text{*Legacy: weaker version of the theorem @{text power_strict_mono},
-used 6 times in NthRoot and Transcendental*}
+text{*Legacy: weaker version of the theorem @{text power_strict_mono}*}
 lemma realpow_less:
      "[|(0::real) < x; x < y; 0 < n|] ==> x ^ n < y ^ n"
 apply (rule power_strict_mono, auto) 
@@ -67,11 +66,9 @@
 lemma realpow_Suc_le_self: "[| 0 \<le> r; r \<le> (1::real) |] ==> r ^ Suc n \<le> r"
 by (insert power_decreasing [of 1 "Suc n" r], simp)
 
-text{*Used ONCE in Transcendental*}
 lemma realpow_Suc_less_one: "[| 0 < r; r < (1::real) |] ==> r ^ Suc n < 1"
 by (insert power_strict_decreasing [of 0 "Suc n" r], simp)
 
-text{*Used ONCE in Lim.ML*}
 lemma realpow_minus_mult [rule_format]:
      "0 < n --> (x::real) ^ (n - 1) * x = x ^ n" 
 apply (simp split add: nat_diff_split)
@@ -140,7 +137,6 @@
 
 subsection{*Various Other Theorems*}
 
-text{*Used several times in Hyperreal/Transcendental.ML*}
 lemma real_sum_squares_cancel_a: "x * x = -(y * y) ==> x = (0::real) & y=0"
   apply (auto dest: real_sum_squares_cancel simp add: real_add_eq_0_iff [symmetric])
   apply (auto dest: real_sum_squares_cancel simp add: add_commute)
@@ -171,7 +167,6 @@
 apply (auto simp add: mult_ac)
 done
 
-text{*Used once: in Hyperreal/Transcendental.ML*}
 lemma real_mult_inverse_cancel2:
      "[|(0::real) < x;0 < x1; x1 * y < x * u |] ==> y * inverse x < u * inverse x1"
 apply (auto dest: real_mult_inverse_cancel simp add: mult_ac)
@@ -272,59 +267,4 @@
 apply (auto simp add: realpow_num_eq_if)
 done
 
-
-ML
-{*
-val realpow_0 = thm "realpow_0";
-val realpow_Suc = thm "realpow_Suc";
-
-val realpow_not_zero = thm "realpow_not_zero";
-val realpow_zero_zero = thm "realpow_zero_zero";
-val realpow_two = thm "realpow_two";
-val realpow_less = thm "realpow_less";
-val realpow_two_le = thm "realpow_two_le";
-val abs_realpow_two = thm "abs_realpow_two";
-val realpow_two_abs = thm "realpow_two_abs";
-val two_realpow_ge_one = thm "two_realpow_ge_one";
-val two_realpow_gt = thm "two_realpow_gt";
-val realpow_Suc_le_self = thm "realpow_Suc_le_self";
-val realpow_Suc_less_one = thm "realpow_Suc_less_one";
-val realpow_minus_mult = thm "realpow_minus_mult";
-val realpow_two_mult_inverse = thm "realpow_two_mult_inverse";
-val realpow_two_minus = thm "realpow_two_minus";
-val realpow_two_disj = thm "realpow_two_disj";
-val realpow_real_of_nat = thm "realpow_real_of_nat";
-val realpow_real_of_nat_two_pos = thm "realpow_real_of_nat_two_pos";
-val realpow_increasing = thm "realpow_increasing";
-val zero_less_realpow_abs_iff = thm "zero_less_realpow_abs_iff";
-val zero_le_realpow_abs = thm "zero_le_realpow_abs";
-val real_of_int_power = thm "real_of_int_power";
-val power_real_number_of = thm "power_real_number_of";
-val real_sum_squares_cancel_a = thm "real_sum_squares_cancel_a";
-val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2";
-val real_squared_diff_one_factored = thm "real_squared_diff_one_factored";
-val real_mult_is_one = thm "real_mult_is_one";
-val real_le_add_half_cancel = thm "real_le_add_half_cancel";
-val real_minus_half_eq = thm "real_minus_half_eq";
-val real_mult_inverse_cancel = thm "real_mult_inverse_cancel";
-val real_mult_inverse_cancel2 = thm "real_mult_inverse_cancel2";
-val inverse_real_of_nat_gt_zero = thm "inverse_real_of_nat_gt_zero";
-val inverse_real_of_nat_ge_zero = thm "inverse_real_of_nat_ge_zero";
-val real_sum_squares_not_zero = thm "real_sum_squares_not_zero";
-val real_sum_squares_not_zero2 = thm "real_sum_squares_not_zero2";
-
-val realpow_divide = thm "realpow_divide";
-val realpow_two_sum_zero_iff = thm "realpow_two_sum_zero_iff";
-val realpow_two_le_add_order = thm "realpow_two_le_add_order";
-val realpow_two_le_add_order2 = thm "realpow_two_le_add_order2";
-val real_sum_square_gt_zero = thm "real_sum_square_gt_zero";
-val real_sum_square_gt_zero2 = thm "real_sum_square_gt_zero2";
-val real_minus_mult_self_le = thm "real_minus_mult_self_le";
-val realpow_square_minus_le = thm "realpow_square_minus_le";
-val realpow_num_eq_if = thm "realpow_num_eq_if";
-val real_num_zero_less_two_pow = thm "real_num_zero_less_two_pow";
-val lemma_realpow_num_two_mono = thm "lemma_realpow_num_two_mono";
-*}
-
-
 end