src/HOL/Hyperreal/Transcendental.thy

--- a/src/HOL/Hyperreal/Transcendental.thy	Wed Jun 30 14:04:58 2004 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Thu Jul 01 12:29:53 2004 +0200
@@ -8,42 +8,42 @@
 Transcendental = NthRoot + Fact + HSeries + EvenOdd + Lim + 
 
 constdefs
-    root :: [nat,real] => real
+    root :: "[nat,real] => real"
     "root n x == (@u. ((0::real) < x --> 0 < u) & (u ^ n = x))"
 
-    sqrt :: real => real
+    sqrt :: "real => real"
     "sqrt x == root 2 x"
 
-    exp :: real => real
+    exp :: "real => real"
     "exp x == suminf(%n. inverse(real (fact n)) * (x ^ n))"
 
-    sin :: real => real
+    sin :: "real => real"
     "sin x == suminf(%n. (if even(n) then 0 else
              ((- 1) ^ ((n - Suc 0) div 2))/(real (fact n))) * x ^ n)"
  
-    diffs :: (nat => real) => nat => real
+    diffs :: "(nat => real) => nat => real"
     "diffs c == (%n. real (Suc n) * c(Suc n))"
 
-    cos :: real => real
+    cos :: "real => real"
     "cos x == suminf(%n. (if even(n) then ((- 1) ^ (n div 2))/(real (fact n)) 
                           else 0) * x ^ n)"
   
-    ln :: real => real
+    ln :: "real => real"
     "ln x == (@u. exp u = x)"
 
-    pi :: real
+    pi :: "real"
     "pi == 2 * (@x. 0 <= (x::real) & x <= 2 & cos x = 0)"
 
-    tan :: real => real
+    tan :: "real => real"
     "tan x == (sin x)/(cos x)"
 
-    arcsin :: real => real
+    arcsin :: "real => real"
     "arcsin y == (@x. -(pi/2) <= x & x <= pi/2 & sin x = y)"
 
-    arcos :: real => real
+    arcos :: "real => real"
     "arcos y == (@x. 0 <= x & x <= pi & cos x = y)"
      
-    arctan :: real => real
+    arctan :: "real => real"
     "arctan y == (@x. -(pi/2) < x & x < pi/2 & tan x = y)"
   
 end