src/HOL/Integ/IntPower.thy

reorganization of HOL/UNITY, moving examples to subdirectories Simple and Comp

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