--- 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)
--- 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;
--- 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";
--- 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"
--- 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"
--- 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;
--- 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 +
--- 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
--- 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