src/HOL/HOL.thy
changeset 3370 5c5fdce3a4e4
parent 3320 3a5e4930fb77
child 3820 46b255e140dc
     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