--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Integ/IntPower.thy	Thu Aug 03 10:52:30 2000 +0200
@@ -0,0 +1,18 @@
+(*  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