Overloading of "^" requires new type class "power", with types "nat" and
authorpaulson
Fri May 30 15:19:58 1997 +0200 (1997-05-30)
changeset 33705c5fdce3a4e4
parent 3369 51ed014406fa
child 3371 80f0d0b2f404
Overloading of "^" requires new type class "power", with types "nat" and
"set" in that class. The operator itself is declared in Nat.thy
src/HOL/HOL.thy
src/HOL/Nat.thy
src/HOL/RelPow.thy
src/HOL/Set.thy
     1.1 --- a/src/HOL/HOL.thy	Fri May 30 15:17:36 1997 +0200
     1.2 +++ b/src/HOL/HOL.thy	Fri May 30 15:19:58 1997 +0200
     1.3 @@ -66,12 +66,14 @@
     1.4  axclass
     1.5    times < term
     1.6  
     1.7 +axclass
     1.8 +  power < term
     1.9 +
    1.10  consts
    1.11 -  "+"           :: ['a::plus, 'a] => 'a             (infixl 65)
    1.12 +  "+"           :: ['a::plus, 'a]  => 'a            (infixl 65)
    1.13    "-"           :: ['a::minus, 'a] => 'a            (infixl 65)
    1.14    "*"           :: ['a::times, 'a] => 'a            (infixl 70)
    1.15 -
    1.16 -
    1.17 +  (*See Nat.thy for "^"*)
    1.18  
    1.19  (** Additional concrete syntax **)
    1.20  
     2.1 --- a/src/HOL/Nat.thy	Fri May 30 15:17:36 1997 +0200
     2.2 +++ b/src/HOL/Nat.thy	Fri May 30 15:19:58 1997 +0200
     2.3 @@ -10,4 +10,7 @@
     2.4  
     2.5  instance nat :: order (le_refl,le_trans,le_anti_sym,nat_less_le)
     2.6  
     2.7 +consts
     2.8 +  "^"           :: ['a::power,nat] => 'a            (infixr 80)
     2.9 +
    2.10  end
     3.1 --- a/src/HOL/RelPow.thy	Fri May 30 15:17:36 1997 +0200
     3.2 +++ b/src/HOL/RelPow.thy	Fri May 30 15:19:58 1997 +0200
     3.3 @@ -8,9 +8,6 @@
     3.4  
     3.5  RelPow = Nat +
     3.6  
     3.7 -consts
     3.8 -  "^" :: "('a * 'a) set => nat => ('a * 'a) set" (infixr 100)
     3.9 -
    3.10  primrec "op ^" nat
    3.11    "R^0 = id"
    3.12    "R^(Suc n) = R O (R^n)"
     4.1 --- a/src/HOL/Set.thy	Fri May 30 15:17:36 1997 +0200
     4.2 +++ b/src/HOL/Set.thy	Fri May 30 15:19:58 1997 +0200
     4.3 @@ -16,7 +16,7 @@
     4.4    set :: (term) term
     4.5  
     4.6  instance
     4.7 -  set :: (term) {ord, minus}
     4.8 +  set :: (term) {ord, minus, power}
     4.9  
    4.10  consts
    4.11    "{}"          :: 'a set                           ("{}")