src/HOL/Real/RealPow.thy
changeset 10309 a7f961fb62c6
parent 9435 c3a13a7d4424
child 11701 3d51fbf81c17
     1.1 --- a/src/HOL/Real/RealPow.thy	Mon Oct 23 22:09:52 2000 +0200
     1.2 +++ b/src/HOL/Real/RealPow.thy	Mon Oct 23 22:10:36 2000 +0200
     1.3 @@ -12,8 +12,7 @@
     1.4  lemmas [arith_split] = abs_split
     1.5  
     1.6  
     1.7 -instance real :: power
     1.8 -  by intro_classes
     1.9 +instance real :: power ..
    1.10  
    1.11  primrec (realpow)
    1.12       realpow_0:   "r ^ 0       = #1"