# HG changeset patch
# User haftmann
# Date 1214975517 -7200
# Node ID b3f8e9bdf9a70357d67e5032e03d8e2c0f586aa8
# Parent  8a7100d33960449476604d93b6fff69c4a52f336
cleaned up some code generator configuration

diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Complex/NSCA.thy
--- a/src/HOL/Complex/NSCA.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Complex/NSCA.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -14,10 +14,9 @@
    SComplex  :: "hcomplex set" where
    "SComplex \<equiv> Standard"
 
-definition
-   stc :: "hcomplex => hcomplex" where
-    --{* standard part map*}
-   "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
+definition --{* standard part map*}
+  stc :: "hcomplex => hcomplex" where 
+  [code func del]: "stc x = (SOME r. x \<in> HFinite & r:SComplex & r @= x)"
 
 
 subsection{*Closure Laws for SComplex, the Standard Complex Numbers*}
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Complex/NSComplex.thy
--- a/src/HOL/Complex/NSComplex.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Complex/NSComplex.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -26,11 +26,11 @@
 
 definition
   hRe :: "hcomplex => hypreal" where
-  "hRe = *f* Re"
+  [code func del]: "hRe = *f* Re"
 
 definition
   hIm :: "hcomplex => hypreal" where
-  "hIm = *f* Im"
+  [code func del]: "hIm = *f* Im"
 
 
   (*------ imaginary unit ----------*)
@@ -43,22 +43,22 @@
 
 definition
   hcnj :: "hcomplex => hcomplex" where
-  "hcnj = *f* cnj"
+  [code func del]: "hcnj = *f* cnj"
 
   (*------------ Argand -------------*)
 
 definition
   hsgn :: "hcomplex => hcomplex" where
-  "hsgn = *f* sgn"
+  [code func del]: "hsgn = *f* sgn"
 
 definition
   harg :: "hcomplex => hypreal" where
-  "harg = *f* arg"
+  [code func del]: "harg = *f* arg"
 
 definition
   (* abbreviation for (cos a + i sin a) *)
   hcis :: "hypreal => hcomplex" where
-  "hcis = *f* cis"
+  [code func del]:"hcis = *f* cis"
 
   (*----- injection from hyperreals -----*)
 
@@ -69,16 +69,16 @@
 definition
   (* abbreviation for r*(cos a + i sin a) *)
   hrcis :: "[hypreal, hypreal] => hcomplex" where
-  "hrcis = *f2* rcis"
+  [code func del]: "hrcis = *f2* rcis"
 
   (*------------ e ^ (x + iy) ------------*)
 definition
   hexpi :: "hcomplex => hcomplex" where
-  "hexpi = *f* expi"
+  [code func del]: "hexpi = *f* expi"
 
 definition
   HComplex :: "[hypreal,hypreal] => hcomplex" where
-  "HComplex = *f2* Complex"
+  [code func del]: "HComplex = *f2* Complex"
 
 lemmas hcomplex_defs [transfer_unfold] =
   hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Hyperreal/HDeriv.thy
--- a/src/HOL/Hyperreal/HDeriv.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/HDeriv.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -27,7 +27,7 @@
 
 definition
   increment :: "[real=>real,real,hypreal] => hypreal" where
-  "increment f x h = (@inc. f NSdifferentiable x &
+  [code func del]: "increment f x h = (@inc. f NSdifferentiable x &
            inc = ( *f* f)(hypreal_of_real x + h) - hypreal_of_real (f x))"
 
 
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Hyperreal/HLim.thy
--- a/src/HOL/Hyperreal/HLim.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/HLim.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -16,18 +16,18 @@
 definition
   NSLIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
             ("((_)/ -- (_)/ --NS> (_))" [60, 0, 60] 60) where
-  "f -- a --NS> L =
+  [code func del]: "f -- a --NS> L =
     (\<forall>x. (x \<noteq> star_of a & x @= star_of a --> ( *f* f) x @= star_of L))"
 
 definition
   isNSCont :: "['a::real_normed_vector => 'b::real_normed_vector, 'a] => bool" where
     --{*NS definition dispenses with limit notions*}
-  "isNSCont f a = (\<forall>y. y @= star_of a -->
+  [code func del]: "isNSCont f a = (\<forall>y. y @= star_of a -->
          ( *f* f) y @= star_of (f a))"
 
 definition
   isNSUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
-  "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
+  [code func del]: "isNSUCont f = (\<forall>x y. x @= y --> ( *f* f) x @= ( *f* f) y)"
 
 
 subsection {* Limits of Functions *}
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Hyperreal/HLog.thy
--- a/src/HOL/Hyperreal/HLog.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/HLog.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -20,14 +20,11 @@
 
 definition
   powhr  :: "[hypreal,hypreal] => hypreal"     (infixr "powhr" 80) where
-  "x powhr a = starfun2 (op powr) x a"
+  [transfer_unfold, code func del]: "x powhr a = starfun2 (op powr) x a"
   
 definition
   hlog :: "[hypreal,hypreal] => hypreal" where
-  "hlog a x = starfun2 log a x"
-
-declare powhr_def [transfer_unfold]
-declare hlog_def [transfer_unfold]
+  [transfer_unfold, code func del]: "hlog a x = starfun2 log a x"
 
 lemma powhr: "(star_n X) powhr (star_n Y) = star_n (%n. (X n) powr (Y n))"
 by (simp add: powhr_def starfun2_star_n)
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Hyperreal/HSEQ.thy
--- a/src/HOL/Hyperreal/HSEQ.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/HSEQ.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -16,7 +16,7 @@
   NSLIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
     ("((_)/ ----NS> (_))" [60, 60] 60) where
     --{*Nonstandard definition of convergence of sequence*}
-  "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
+  [code func del]: "X ----NS> L = (\<forall>N \<in> HNatInfinite. ( *f* X) N \<approx> star_of L)"
 
 definition
   nslim :: "(nat => 'a::real_normed_vector) => 'a" where
@@ -31,12 +31,12 @@
 definition
   NSBseq :: "(nat => 'a::real_normed_vector) => bool" where
     --{*Nonstandard definition for bounded sequence*}
-  "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
+  [code func del]: "NSBseq X = (\<forall>N \<in> HNatInfinite. ( *f* X) N : HFinite)"
 
 definition
   NSCauchy :: "(nat => 'a::real_normed_vector) => bool" where
     --{*Nonstandard definition*}
-  "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
+  [code func del]: "NSCauchy X = (\<forall>M \<in> HNatInfinite. \<forall>N \<in> HNatInfinite. ( *f* X) M \<approx> ( *f* X) N)"
 
 subsection {* Limits of Sequences *}
 
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Hyperreal/HSeries.thy
--- a/src/HOL/Hyperreal/HSeries.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/HSeries.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -13,7 +13,7 @@
 
 definition
   sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal" where
-  "sumhr = 
+  [code func del]: "sumhr = 
       (%(M,N,f). starfun2 (%m n. setsum f {m..<n}) M N)"
 
 definition
@@ -22,7 +22,7 @@
 
 definition
   NSsummable :: "(nat=>real) => bool" where
-  "NSsummable f = (\<exists>s. f NSsums s)"
+  [code func del]: "NSsummable f = (\<exists>s. f NSsums s)"
 
 definition
   NSsuminf   :: "(nat=>real) => real" where
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/HyperDef.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -47,7 +47,7 @@
 begin
 
 definition
-  star_scaleR_def [transfer_unfold]: "scaleR r \<equiv> *f* (scaleR r)"
+  star_scaleR_def [transfer_unfold, code func del]: "scaleR r \<equiv> *f* (scaleR r)"
 
 instance ..
 
@@ -111,9 +111,7 @@
 
 definition
   of_hypreal :: "hypreal \<Rightarrow> 'a::real_algebra_1 star" where
-  "of_hypreal = *f* of_real"
-
-declare of_hypreal_def [transfer_unfold]
+  [transfer_unfold, code func del]: "of_hypreal = *f* of_real"
 
 lemma Standard_of_hypreal [simp]:
   "r \<in> Standard \<Longrightarrow> of_hypreal r \<in> Standard"
@@ -427,11 +425,9 @@
 
 subsection{*Powers with Hypernatural Exponents*}
 
-definition
+definition pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
+  hyperpow_def [transfer_unfold, code func del]: "R pow N = ( *f2* op ^) R N"
   (* hypernatural powers of hyperreals *)
-  pow :: "['a::power star, nat star] \<Rightarrow> 'a star" (infixr "pow" 80) where
-  hyperpow_def [transfer_unfold]:
-  "R pow N = ( *f2* op ^) R N"
 
 lemma Standard_hyperpow [simp]:
   "\<lbrakk>r \<in> Standard; n \<in> Standard\<rbrakk> \<Longrightarrow> r pow n \<in> Standard"
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Hyperreal/HyperNat.thy
--- a/src/HOL/Hyperreal/HyperNat.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/HyperNat.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -19,7 +19,7 @@
 
 definition
   hSuc :: "hypnat => hypnat" where
-  hSuc_def [transfer_unfold]: "hSuc = *f* Suc"
+  hSuc_def [transfer_unfold, code func del]: "hSuc = *f* Suc"
 
 subsection{*Properties Transferred from Naturals*}
 
@@ -367,7 +367,7 @@
 
 definition
   of_hypnat :: "hypnat \<Rightarrow> 'a::semiring_1_cancel star" where
-  of_hypnat_def [transfer_unfold]: "of_hypnat = *f* of_nat"
+  of_hypnat_def [transfer_unfold, code func del]: "of_hypnat = *f* of_nat"
 
 lemma of_hypnat_0 [simp]: "of_hypnat 0 = 0"
 by transfer (rule of_nat_0)
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Hyperreal/Integration.thy
--- a/src/HOL/Hyperreal/Integration.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/Integration.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -16,29 +16,29 @@
   --{*Partitions and tagged partitions etc.*}
 
   partition :: "[(real*real),nat => real] => bool" where
-  "partition = (%(a,b) D. D 0 = a &
+  [code func del]: "partition = (%(a,b) D. D 0 = a &
                          (\<exists>N. (\<forall>n < N. D(n) < D(Suc n)) &
                               (\<forall>n \<ge> N. D(n) = b)))"
 
 definition
   psize :: "(nat => real) => nat" where
-  "psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
+  [code func del]:"psize D = (SOME N. (\<forall>n < N. D(n) < D(Suc n)) &
                       (\<forall>n \<ge> N. D(n) = D(N)))"
 
 definition
   tpart :: "[(real*real),((nat => real)*(nat =>real))] => bool" where
-  "tpart = (%(a,b) (D,p). partition(a,b) D &
+  [code func del]:"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*}
 
 definition
   gauge :: "[real => bool, real => real] => bool" where
-  "gauge E g = (\<forall>x. E x --> 0 < g(x))"
+  [code func del]:"gauge E g = (\<forall>x. E x --> 0 < g(x))"
 
 definition
   fine :: "[real => real, ((nat => real)*(nat => real))] => bool" where
-  "fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))"
+  [code func del]:"fine = (%g (D,p). \<forall>n. n < (psize D) --> D(Suc n) - D(n) < g(p n))"
 
   --{*Riemann sum*}
 
@@ -50,7 +50,7 @@
 
 definition
   Integral :: "[(real*real),real=>real,real] => bool" where
-  "Integral = (%(a,b) f k. \<forall>e > 0.
+  [code func del]: "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)))"
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -16,7 +16,7 @@
 definition
   LIM :: "['a::real_normed_vector => 'b::real_normed_vector, 'a, 'b] => bool"
         ("((_)/ -- (_)/ --> (_))" [60, 0, 60] 60) where
-  "f -- a --> L =
+  [code func del]: "f -- a --> L =
      (\<forall>r > 0. \<exists>s > 0. \<forall>x. x \<noteq> a & norm (x - a) < s
         --> norm (f x - L) < r)"
 
@@ -26,7 +26,7 @@
 
 definition
   isUCont :: "['a::real_normed_vector => 'b::real_normed_vector] => bool" where
-  "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)"
+  [code func del]: "isUCont f = (\<forall>r>0. \<exists>s>0. \<forall>x y. norm (x - y) < s \<longrightarrow> norm (f x - f y) < r)"
 
 
 subsection {* Limits of Functions *}
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/NSA.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -13,19 +13,19 @@
 
 definition
   hnorm :: "'a::norm star \<Rightarrow> real star" where
-  "hnorm = *f* norm"
+  [transfer_unfold]: "hnorm = *f* norm"
 
 definition
   Infinitesimal  :: "('a::real_normed_vector) star set" where
-  "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
+  [code func del]: "Infinitesimal = {x. \<forall>r \<in> Reals. 0 < r --> hnorm x < r}"
 
 definition
   HFinite :: "('a::real_normed_vector) star set" where
-  "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
+  [code func del]: "HFinite = {x. \<exists>r \<in> Reals. hnorm x < r}"
 
 definition
   HInfinite :: "('a::real_normed_vector) star set" where
-  "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
+  [code func del]: "HInfinite = {x. \<forall>r \<in> Reals. r < hnorm x}"
 
 definition
   approx :: "['a::real_normed_vector star, 'a star] => bool"  (infixl "@=" 50) where
@@ -58,10 +58,7 @@
 
 definition
   scaleHR :: "real star \<Rightarrow> 'a star \<Rightarrow> 'a::real_normed_vector star" where
-  "scaleHR = starfun2 scaleR"
-
-declare hnorm_def [transfer_unfold]
-declare scaleHR_def [transfer_unfold]
+  [transfer_unfold, code func del]: "scaleHR = starfun2 scaleR"
 
 lemma Standard_hnorm [simp]: "x \<in> Standard \<Longrightarrow> hnorm x \<in> Standard"
 by (simp add: hnorm_def)
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/SEQ.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -15,13 +15,13 @@
 definition
   Zseq :: "[nat \<Rightarrow> 'a::real_normed_vector] \<Rightarrow> bool" where
     --{*Standard definition of sequence converging to zero*}
-  "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
+  [code func del]: "Zseq X = (\<forall>r>0. \<exists>no. \<forall>n\<ge>no. norm (X n) < r)"
 
 definition
   LIMSEQ :: "[nat => 'a::real_normed_vector, 'a] => bool"
     ("((_)/ ----> (_))" [60, 60] 60) where
     --{*Standard definition of convergence of sequence*}
-  "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
+  [code func del]: "X ----> L = (\<forall>r. 0 < r --> (\<exists>no. \<forall>n. no \<le> n --> norm (X n - L) < r))"
 
 definition
   lim :: "(nat => 'a::real_normed_vector) => 'a" where
@@ -36,22 +36,22 @@
 definition
   Bseq :: "(nat => 'a::real_normed_vector) => bool" where
     --{*Standard definition for bounded sequence*}
-  "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
+  [code func del]: "Bseq X = (\<exists>K>0.\<forall>n. norm (X n) \<le> K)"
 
 definition
   monoseq :: "(nat=>real)=>bool" where
     --{*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))"
+  [code func del]: "monoseq X = ((\<forall>m. \<forall>n\<ge>m. X m \<le> X n) | (\<forall>m. \<forall>n\<ge>m. X n \<le> X m))"
 
 definition
   subseq :: "(nat => nat) => bool" where
     --{*Definition of subsequence*}
-  "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
+  [code func del]:   "subseq f = (\<forall>m. \<forall>n>m. (f m) < (f n))"
 
 definition
   Cauchy :: "(nat => 'a::real_normed_vector) => bool" where
     --{*Standard definition of the Cauchy condition*}
-  "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
+  [code func del]: "Cauchy X = (\<forall>e>0. \<exists>M. \<forall>m \<ge> M. \<forall>n \<ge> M. norm (X m - X n) < e)"
 
 
 subsection {* Bounded Sequences *}
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Hyperreal/Star.thy
--- a/src/HOL/Hyperreal/Star.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/Star.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -17,12 +17,12 @@
 
 definition
   InternalSets :: "'a star set set" where
-  "InternalSets = {X. \<exists>As. X = *sn* As}"
+  [code func del]: "InternalSets = {X. \<exists>As. X = *sn* As}"
 
 definition
   (* nonstandard extension of function *)
   is_starext  :: "['a star => 'a star, 'a => 'a] => bool" where
-  "is_starext F f = (\<forall>x y. \<exists>X \<in> Rep_star(x). \<exists>Y \<in> Rep_star(y).
+  [code func del]: "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)))"
 
 definition
@@ -32,7 +32,7 @@
 
 definition
   InternalFuns :: "('a star => 'b star) set" where
-  "InternalFuns = {X. \<exists>F. X = *fn* F}"
+  [code func del]:"InternalFuns = {X. \<exists>F. X = *fn* F}"
 
 
 (*--------------------------------------------------------
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Hyperreal/StarDef.thy
--- a/src/HOL/Hyperreal/StarDef.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Hyperreal/StarDef.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -290,9 +290,8 @@
 
 subsection {* Internal predicates *}
 
-definition
-  unstar :: "bool star \<Rightarrow> bool" where
-  "unstar b = (b = star_of True)"
+definition unstar :: "bool star \<Rightarrow> bool" where
+  [code func del]: "unstar b \<longleftrightarrow> 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)
@@ -433,7 +432,7 @@
 begin
 
 definition
-  star_zero_def:    "0 \<equiv> star_of 0"
+  star_zero_def [code func del]:    "0 \<equiv> star_of 0"
 
 instance ..
 
@@ -443,7 +442,7 @@
 begin
 
 definition
-  star_one_def:     "1 \<equiv> star_of 1"
+  star_one_def [code func del]:     "1 \<equiv> star_of 1"
 
 instance ..
 
@@ -453,7 +452,7 @@
 begin
 
 definition
-  star_add_def:     "(op +) \<equiv> *f2* (op +)"
+  star_add_def [code func del]:     "(op +) \<equiv> *f2* (op +)"
 
 instance ..
 
@@ -463,7 +462,7 @@
 begin
 
 definition
-  star_mult_def:    "(op *) \<equiv> *f2* (op *)"
+  star_mult_def [code func del]:    "(op *) \<equiv> *f2* (op *)"
 
 instance ..
 
@@ -473,7 +472,7 @@
 begin
 
 definition
-  star_minus_def:   "uminus \<equiv> *f* uminus"
+  star_minus_def [code func del]:   "uminus \<equiv> *f* uminus"
 
 instance ..
 
@@ -483,7 +482,7 @@
 begin
 
 definition
-  star_diff_def:    "(op -) \<equiv> *f2* (op -)"
+  star_diff_def [code func del]:    "(op -) \<equiv> *f2* (op -)"
 
 instance ..
 
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Lambda/WeakNorm.thy
--- a/src/HOL/Lambda/WeakNorm.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Lambda/WeakNorm.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -418,33 +418,27 @@
   CodeTarget.add_undefined "SML" "arbitrary" "(raise Fail \"arbitrary\")"
 *}
 
-definition
-  int_of_nat :: "nat \<Rightarrow> int" where
+definition int_of_nat :: "nat \<Rightarrow> int" where
   "int_of_nat = of_nat"
 
-export_code type_NF nat int_of_nat in SML module_name Norm
-
 ML {*
-val nat_of_int = Norm.nat;
-val int_of_nat = Norm.int_of_nat;
-
 fun dBtype_of_typ (Type ("fun", [T, U])) =
-      Norm.Fun (dBtype_of_typ T, dBtype_of_typ U)
+      @{code Fun} (dBtype_of_typ T, dBtype_of_typ U)
   | dBtype_of_typ (TFree (s, _)) = (case explode s of
-        ["'", a] => Norm.Atom (nat_of_int (ord a - 97))
+        ["'", a] => @{code Atom} (@{code nat} (ord a - 97))
       | _ => error "dBtype_of_typ: variable name")
   | dBtype_of_typ _ = error "dBtype_of_typ: bad type";
 
-fun dB_of_term (Bound i) = Norm.Var (nat_of_int i)
-  | dB_of_term (t $ u) = Norm.App (dB_of_term t, dB_of_term u)
-  | dB_of_term (Abs (_, _, t)) = Norm.Abs (dB_of_term t)
+fun dB_of_term (Bound i) = @{code dB.Var} (@{code nat} i)
+  | dB_of_term (t $ u) = @{code dB.App} (dB_of_term t, dB_of_term u)
+  | dB_of_term (Abs (_, _, t)) = @{code dB.Abs} (dB_of_term t)
   | dB_of_term _ = error "dB_of_term: bad term";
 
-fun term_of_dB Ts (Type ("fun", [T, U])) (Norm.Abs dBt) =
+fun term_of_dB Ts (Type ("fun", [T, U])) (@{code dB.Abs} dBt) =
       Abs ("x", T, term_of_dB (T :: Ts) U dBt)
   | term_of_dB Ts _ dBt = term_of_dB' Ts dBt
-and term_of_dB' Ts (Norm.Var n) = Bound (int_of_nat n)
-  | term_of_dB' Ts (Norm.App (dBt, dBu)) =
+and term_of_dB' Ts (@{code dB.Var} n) = Bound (@{code int_of_nat} n)
+  | term_of_dB' Ts (@{code dB.App} (dBt, dBu)) =
       let val t = term_of_dB' Ts dBt
       in case fastype_of1 (Ts, t) of
           Type ("fun", [T, U]) => t $ term_of_dB Ts T dBu
@@ -453,30 +447,28 @@
   | term_of_dB' _ _ = error "term_of_dB: term not in normal form";
 
 fun typing_of_term Ts e (Bound i) =
-      Norm.Vara (e, nat_of_int i, dBtype_of_typ (nth Ts i))
+      @{code Var} (e, @{code nat} i, dBtype_of_typ (nth Ts i))
   | typing_of_term Ts e (t $ u) = (case fastype_of1 (Ts, t) of
-        Type ("fun", [T, U]) => Norm.Appb (e, dB_of_term t,
+        Type ("fun", [T, U]) => @{code App} (e, dB_of_term t,
           dBtype_of_typ T, dBtype_of_typ U, dB_of_term u,
           typing_of_term Ts e t, typing_of_term Ts e u)
       | _ => error "typing_of_term: function type expected")
   | typing_of_term Ts e (Abs (s, T, t)) =
       let val dBT = dBtype_of_typ T
-      in Norm.Absb (e, dBT, dB_of_term t,
+      in @{code Abs} (e, dBT, dB_of_term t,
         dBtype_of_typ (fastype_of1 (T :: Ts, t)),
-        typing_of_term (T :: Ts) (Norm.shift e Norm.Zero_nat dBT) t)
+        typing_of_term (T :: Ts) (@{code shift} e @{code "0::nat"} dBT) t)
       end
   | typing_of_term _ _ _ = error "typing_of_term: bad term";
 
 fun dummyf _ = error "dummy";
-*}
 
-ML {*
 val ct1 = @{cterm "%f. ((%f x. f (f (f x))) ((%f x. f (f (f (f x)))) f))"};
-val (dB1, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct1));
+val (dB1, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct1));
 val ct1' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct1)) dB1);
 
 val ct2 = @{cterm "%f x. (%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) ((%x. f x x) x)))))"};
-val (dB2, _) = Norm.type_NF (typing_of_term [] dummyf (term_of ct2));
+val (dB2, _) = @{code type_NF} (typing_of_term [] dummyf (term_of ct2));
 val ct2' = cterm_of @{theory} (term_of_dB [] (#T (rep_cterm ct2)) dB2);
 *}
 
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Library/Univ_Poly.thy
--- a/src/HOL/Library/Univ_Poly.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Library/Univ_Poly.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -72,7 +72,7 @@
 
 definition (in semiring_0)
   divides :: "'a list \<Rightarrow> 'a list \<Rightarrow> bool"  (infixl "divides" 70) where
-  "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
+  [code func del]: "p1 divides p2 = (\<exists>q. poly p2 = poly(p1 *** q))"
 
     --{*order of a polynomial*}
 definition (in ring_1) order :: "'a => 'a list => nat" where
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Real/ContNotDenum.thy
--- a/src/HOL/Real/ContNotDenum.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Real/ContNotDenum.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -393,16 +393,17 @@
 
 subsubsection {* Definition *}
 
-consts newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)"
-primrec
-"newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
-"newInt (Suc n) f =
-  (SOME e. (\<exists>e1 e2.
-   e1 < e2 \<and>
-   e = closed_int e1 e2 \<and>
-   e \<subseteq> (newInt n f) \<and>
-   (f (Suc n)) \<notin> e)
-  )"
+primrec newInt :: "nat \<Rightarrow> (nat \<Rightarrow> real) \<Rightarrow> (real set)" where
+  "newInt 0 f = closed_int (f 0 + 1) (f 0 + 2)"
+  | "newInt (Suc n) f =
+      (SOME e. (\<exists>e1 e2.
+       e1 < e2 \<and>
+       e = closed_int e1 e2 \<and>
+       e \<subseteq> (newInt n f) \<and>
+       (f (Suc n)) \<notin> e)
+      )"
+
+declare newInt.simps [code func del]
 
 subsubsection {* Properties *}
 
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Real/RComplete.thy
--- a/src/HOL/Real/RComplete.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Real/RComplete.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -434,7 +434,7 @@
 
 definition
   floor :: "real => int" where
-  "floor r = (LEAST n::int. r < real (n+1))"
+  [code func del]: "floor r = (LEAST n::int. r < real (n+1))"
 
 definition
   ceiling :: "real => int" where
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/Real/RealVector.thy
--- a/src/HOL/Real/RealVector.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/Real/RealVector.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -264,7 +264,7 @@
 
 definition
   Reals :: "'a::real_algebra_1 set" where
-  "Reals \<equiv> range of_real"
+  [code func del]: "Reals \<equiv> range of_real"
 
 notation (xsymbols)
   Reals  ("\<real>")
diff -r 8a7100d33960 -r b3f8e9bdf9a7 src/HOL/ex/ExecutableContent.thy
--- a/src/HOL/ex/ExecutableContent.thy	Tue Jul 01 21:30:12 2008 +0200
+++ b/src/HOL/ex/ExecutableContent.thy	Wed Jul 02 07:11:57 2008 +0200
@@ -33,63 +33,25 @@
 
 (*FIXME distribute to theories*)
 declare divides_def [code func del] -- "Univ_Poly"
-declare unstar_def [code func del] -- "StarDef"
-declare star_one_def [code func del] -- "StarDef"
-declare star_mult_def [code func del] -- "StarDef"
-declare star_add_def [code func del] -- "StarDef"
-declare star_zero_def [code func del] -- "StarDef"
 declare star_minus_def [code func del] -- "StarDef"
-declare star_diff_def [code func del] -- "StarDef"
-declare Reals_def [code func del] -- "RealVector"
-declare star_scaleR_def [code func del] -- "HyperDef"
-declare hyperpow_def [code func del] -- HyperDef
-declare Infinitesimal_def [code func del] -- NSA
-declare HFinite_def [code func del] -- NSA
-declare floor_def [code func del] -- RComplete
-declare LIMSEQ_def [code func del] -- SEQ
-declare partition_def [code func del] -- Integration
-declare Integral_def [code func del] -- Integration
-declare tpart_def [code func del] -- Integration
-declare psize_def [code func del] -- Integration
-declare gauge_def [code func del] -- Integration
-declare fine_def [code func del] -- Integration
-declare sumhr_def [code func del] -- HSeries
-declare NSsummable_def [code func del] -- HSeries
-declare NSLIMSEQ_def [code func del] -- HSEQ
-declare newInt.simps [code func del] -- ContNotDenum
-declare LIM_def [code func del] -- Lim
-declare NSLIM_def [code func del] -- HLim
-declare HComplex_def [code func del]
-declare of_hypnat_def [code func del]
-declare InternalSets_def [code func del]
-declare InternalFuns_def [code func del]
-declare increment_def [code func del]
-declare is_starext_def [code func del]
-declare hrcis_def [code func del]
-declare hexpi_def [code func del]
-declare hsgn_def [code func del]
-declare hcnj_def [code func del]
-declare hcis_def [code func del]
-declare harg_def [code func del]
-declare isNSUCont_def [code func del]
-declare hRe_def [code func del]
-declare hIm_def [code func del]
-declare HInfinite_def [code func del]
-declare hSuc_def [code func del]
-declare NSCauchy_def [code func del]
-declare of_hypreal_def [code func del]
-declare isNSCont_def [code func del]
+declare Zseq_def [code func del]
+declare Bseq_def [code func del]
 declare monoseq_def [code func del]
-declare scaleHR_def [code func del]
-declare isUCont_def [code func del]
-declare NSBseq_def [code func del]
+declare Cauchy_def [code func del]
 declare subseq_def [code func del]
-declare Cauchy_def [code func del]
 declare powhr_def [code func del]
 declare hlog_def [code func del]
-declare Zseq_def [code func del]
-declare Bseq_def [code func del]
+declare scaleHR_def [code func del]
 declare stc_def [code func del]
+declare increment_def [code func del]
+declare of_hypreal_def [code func del]
+declare HInfinite_def [code func del]
+declare is_starext_def [code func del]
+declare isNSUCont_def [code func del]
+declare isNSCont_def [code func del]
+declare isUCont_def [code func del]
+declare NSCauchy_def [code func del]
+declare NSBseq_def [code func del]
 
 setup {*
   Code.del_funcs