src/HOL/Integ/IntPower.thy

lemma Least_mono moved from Typedef.thy to Set.thy;

(*  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