Improved efficiency of code generated for functions int and nat.
(* Title: IntPower.thy
ID: $Id$
Author: Thomas M. Rasmussen
Copyright 2000 University of Cambridge
Integer powers
*)
IntPower = IntDiv +
instance
int :: {power}
primrec
power_0 "p ^ 0 = 1"
power_Suc "p ^ (Suc n) = (p::int) * (p ^ n)"
end