# HG changeset patch
# User haftmann
# Date 1192170348 -7200
# Node ID ebd5f4cc7118fb8f11da5df8a378b33e7bdcdc7d
# Parent  c26e0166e568f53b89a438b9e693e48a04fcaf6a
moved class power to theory Power

diff -r c26e0166e568 -r ebd5f4cc7118 NEWS
--- a/NEWS	Fri Oct 12 08:25:47 2007 +0200
+++ b/NEWS	Fri Oct 12 08:25:48 2007 +0200
@@ -741,19 +741,21 @@
 
     HOL.abs ~> HOL.minus_class.abs
     HOL.divide ~> HOL.divide_class.divide
-    Nat.power ~> Nat.power_class.power
+    Nat.power ~> Power.power_class.power
     Nat.size ~> Nat.size_class.size
     Numeral.number_of ~> Numeral.number_class.number_of
-    FixedPoint.Inf ~> FixedPoint.complete_lattice_class.Inf
-    FixedPoint.Sup ~> FixedPoint.complete_lattice_class.Sup
+    FixedPoint.Inf ~> Lattices.complete_lattice_class.Inf
+    FixedPoint.Sup ~> Lattices.complete_lattice_class.Sup
     Orderings.min ~> Orderings.ord_class.min
     Orderings.max ~> Orderings.ord_class.max
 
+INCOMPATIBILITY.
+
 * New class "default" with associated constant "default".
 
 * New constant "undefined" with axiom "undefined x = undefined".
 
-* primrec: missing cases mapped to "undefined" instead of "arbitrary"
+* primrec: missing cases mapped to "undefined" instead of "arbitrary".
 
 * New function listsum :: 'a list => 'a for arbitrary monoids.
 Special syntax: "SUM x <- xs. f x" (and latex variants)
diff -r c26e0166e568 -r ebd5f4cc7118 src/HOL/Import/Generate-HOL/GenHOL4Base.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Oct 12 08:25:47 2007 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Base.thy	Fri Oct 12 08:25:48 2007 +0200
@@ -189,7 +189,7 @@
   MAX          > Orderings.ord_class.max    :: "[nat,nat]=>nat"
   DIV          > Divides.div_class.div :: "[nat,nat]=>nat"
   MOD          > Divides.div_class.mod :: "[nat,nat]=>nat"
-  EXP          > Nat.power_class.power :: "[nat,nat]=>nat";
+  EXP          > Power.power_class.power :: "[nat,nat]=>nat";
 
 end_import;
 
diff -r c26e0166e568 -r ebd5f4cc7118 src/HOL/Import/Generate-HOL/GenHOL4Real.thy
--- a/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Fri Oct 12 08:25:47 2007 +0200
+++ b/src/HOL/Import/Generate-HOL/GenHOL4Real.thy	Fri Oct 12 08:25:48 2007 +0200
@@ -54,7 +54,7 @@
   real_lte    > HOL.ord_class.less_eq :: "[real,real] => bool"
   real_sub    > HOL.minus    :: "[real,real] => real"
   "/"         > HOL.divide   :: "[real,real] => real"
-  pow         > Nat.power    :: "[real,nat] => real"
+  pow         > Power.power_class.power    :: "[real,nat] => real"
   abs         > HOL.abs      :: "real => real"
   real_of_num > RealDef.real :: "nat => real";
 
diff -r c26e0166e568 -r ebd5f4cc7118 src/HOL/Import/HOL/arithmetic.imp
--- a/src/HOL/Import/HOL/arithmetic.imp	Fri Oct 12 08:25:47 2007 +0200
+++ b/src/HOL/Import/HOL/arithmetic.imp	Fri Oct 12 08:25:48 2007 +0200
@@ -17,7 +17,7 @@
   "MIN" > "Orderings.ord_class.min" :: "nat => nat => nat"
   "MAX" > "Orderings.ord_class.max" :: "nat => nat => nat"
   "FUNPOW" > "HOL4Compat.FUNPOW"
-  "EXP" > "Nat.power_class.power" :: "nat => nat => nat"
+  "EXP" > "Power.power_class.power" :: "nat => nat => nat"
   "DIV" > "Divides.div_class.div" :: "nat => nat => nat"
   "MOD" > "Divides.div_class.mod" :: "nat => nat => nat"
   "ALT_ZERO" > "HOL4Compat.ALT_ZERO"
diff -r c26e0166e568 -r ebd5f4cc7118 src/HOL/Import/HOL/real.imp
--- a/src/HOL/Import/HOL/real.imp	Fri Oct 12 08:25:47 2007 +0200
+++ b/src/HOL/Import/HOL/real.imp	Fri Oct 12 08:25:48 2007 +0200
@@ -15,7 +15,7 @@
   "real_lte" > "HOL.ord_class.less_eq" :: "real => real => bool"
   "real_gt" > "HOL4Compat.real_gt"
   "real_ge" > "HOL4Compat.real_ge"
-  "pow" > "Nat.power_class.power" :: "real => nat => real"
+  "pow" > "Power.power_class.power" :: "real => nat => real"
   "abs" > "HOL.minus_class.abs" :: "real => real"
   "/" > "HOL.divides_class.divide" :: "real => real => real"
 
diff -r c26e0166e568 -r ebd5f4cc7118 src/HOL/Library/comm_ring.ML
--- a/src/HOL/Library/comm_ring.ML	Fri Oct 12 08:25:47 2007 +0200
+++ b/src/HOL/Library/comm_ring.ML	Fri Oct 12 08:25:48 2007 +0200
@@ -61,7 +61,7 @@
       polex_mul T $ reif_polex T vs a $ reif_polex T vs b
   | reif_polex T vs (Const (@{const_name HOL.uminus}, _) $ a) =
       polex_neg T $ reif_polex T vs a
-  | reif_polex T vs (Const (@{const_name Nat.power}, _) $ a $ n) =
+  | reif_polex T vs (Const (@{const_name Power.power}, _) $ a $ n) =
       polex_pow T $ reif_polex T vs a $ n
   | reif_polex T vs t = polex_pol T $ reif_pol T vs t;
 
diff -r c26e0166e568 -r ebd5f4cc7118 src/HOL/Power.thy
--- a/src/HOL/Power.thy	Fri Oct 12 08:25:47 2007 +0200
+++ b/src/HOL/Power.thy	Fri Oct 12 08:25:48 2007 +0200
@@ -11,6 +11,9 @@
 imports Nat
 begin
 
+class power = type +
+  fixes power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"            (infixr "\<^loc>^" 80)
+
 subsection{*Powers for Arbitrary Monoids*}
 
 class recpower = monoid_mult + power +
diff -r c26e0166e568 -r ebd5f4cc7118 src/HOL/Relation_Power.thy
--- a/src/HOL/Relation_Power.thy	Fri Oct 12 08:25:47 2007 +0200
+++ b/src/HOL/Relation_Power.thy	Fri Oct 12 08:25:48 2007 +0200
@@ -7,7 +7,7 @@
 header{*Powers of Relations and Functions*}
 
 theory Relation_Power
-imports Nat
+imports Power
 begin
 
 instance
diff -r c26e0166e568 -r ebd5f4cc7118 src/HOL/Tools/Qelim/presburger.ML
--- a/src/HOL/Tools/Qelim/presburger.ML	Fri Oct 12 08:25:47 2007 +0200
+++ b/src/HOL/Tools/Qelim/presburger.ML	Fri Oct 12 08:25:48 2007 +0200
@@ -62,7 +62,7 @@
  | Const(@{const_name "HOL.plus"},_)$l$r => isnum l andalso isnum r
  | Const(@{const_name "HOL.times"},_)$l$r => isnum l andalso isnum r
  | Const(@{const_name "HOL.minus"},_)$l$r => isnum l andalso isnum r
- | Const(@{const_name "Nat.power"},_)$l$r => isnum l andalso isnum r
+ | Const(@{const_name "Power.power"},_)$l$r => isnum l andalso isnum r
  | Const(@{const_name "Divides.mod"},_)$l$r => isnum l andalso isnum r
  | Const(@{const_name "Divides.div"},_)$l$r => isnum l andalso isnum r
  | _ => can HOLogic.dest_number t orelse can HOLogic.dest_nat t