1.1 --- a/src/HOL/NSA/NSComplex.thy	Fri Oct 10 06:45:50 2008 +0200
     1.2 +++ b/src/HOL/NSA/NSComplex.thy	Fri Oct 10 06:45:53 2008 +0200
     1.3 @@ -26,11 +26,11 @@
     1.4  
     1.5  definition
     1.6    hRe :: "hcomplex => hypreal" where
     1.7 -  [code func del]: "hRe = *f* Re"
     1.8 +  [code del]: "hRe = *f* Re"
     1.9  
    1.10  definition
    1.11    hIm :: "hcomplex => hypreal" where
    1.12 -  [code func del]: "hIm = *f* Im"
    1.13 +  [code del]: "hIm = *f* Im"
    1.14  
    1.15  
    1.16    (*------ imaginary unit ----------*)
    1.17 @@ -43,22 +43,22 @@
    1.18  
    1.19  definition
    1.20    hcnj :: "hcomplex => hcomplex" where
    1.21 -  [code func del]: "hcnj = *f* cnj"
    1.22 +  [code del]: "hcnj = *f* cnj"
    1.23  
    1.24    (*------------ Argand -------------*)
    1.25  
    1.26  definition
    1.27    hsgn :: "hcomplex => hcomplex" where
    1.28 -  [code func del]: "hsgn = *f* sgn"
    1.29 +  [code del]: "hsgn = *f* sgn"
    1.30  
    1.31  definition
    1.32    harg :: "hcomplex => hypreal" where
    1.33 -  [code func del]: "harg = *f* arg"
    1.34 +  [code del]: "harg = *f* arg"
    1.35  
    1.36  definition
    1.37    (* abbreviation for (cos a + i sin a) *)
    1.38    hcis :: "hypreal => hcomplex" where
    1.39 -  [code func del]:"hcis = *f* cis"
    1.40 +  [code del]:"hcis = *f* cis"
    1.41  
    1.42    (*----- injection from hyperreals -----*)
    1.43  
    1.44 @@ -69,16 +69,16 @@
    1.45  definition
    1.46    (* abbreviation for r*(cos a + i sin a) *)
    1.47    hrcis :: "[hypreal, hypreal] => hcomplex" where
    1.48 -  [code func del]: "hrcis = *f2* rcis"
    1.49 +  [code del]: "hrcis = *f2* rcis"
    1.50  
    1.51    (*------------ e ^ (x + iy) ------------*)
    1.52  definition
    1.53    hexpi :: "hcomplex => hcomplex" where
    1.54 -  [code func del]: "hexpi = *f* expi"
    1.55 +  [code del]: "hexpi = *f* expi"
    1.56  
    1.57  definition
    1.58    HComplex :: "[hypreal,hypreal] => hcomplex" where
    1.59 -  [code func del]: "HComplex = *f2* Complex"
    1.60 +  [code del]: "HComplex = *f2* Complex"
    1.61  
    1.62  lemmas hcomplex_defs [transfer_unfold] =
    1.63    hRe_def hIm_def iii_def hcnj_def hsgn_def harg_def hcis_def