- Installed specific code generator for equality enforcing that
arguments do not have function types, which would result in
an error message during compilation.
- Added test case generators for basic types.
(* Title : HOL/Real/RealPow.thy
ID : $Id$
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
Description : Natural powers theory
*)
theory RealPow = RealAbs:
(*belongs to theory RealAbs*)
lemmas [arith_split] = abs_split
instance real :: power ..
primrec (realpow)
realpow_0: "r ^ 0 = 1"
realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)"
end