lemmas [arith_split] = abs_split (*belongs to theory RealAbs*);
authorwenzelm
Tue Jul 25 00:03:39 2000 +0200 (2000-07-25)
changeset 9435c3a13a7d4424
parent 9434 d2fa043ab24f
child 9436 62bb04ab4b01
lemmas [arith_split] = abs_split (*belongs to theory RealAbs*);
src/HOL/Real/RealPow.thy
     1.1 --- a/src/HOL/Real/RealPow.thy	Tue Jul 25 00:02:52 2000 +0200
     1.2 +++ b/src/HOL/Real/RealPow.thy	Tue Jul 25 00:03:39 2000 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title       : RealPow.thy
     1.5 +(*  Title       : HOL/Real/RealPow.thy
     1.6      ID          : $Id$
     1.7      Author      : Jacques D. Fleuriot  
     1.8      Copyright   : 1998  University of Cambridge
     1.9 @@ -6,12 +6,17 @@
    1.10  
    1.11  *)
    1.12  
    1.13 -RealPow = RealAbs +
    1.14 +theory RealPow = RealAbs:
    1.15  
    1.16 -instance real :: {power}
    1.17 +(*belongs to theory RealAbs*)
    1.18 +lemmas [arith_split] = abs_split
    1.19 +
    1.20 +
    1.21 +instance real :: power
    1.22 +  by intro_classes
    1.23  
    1.24  primrec (realpow)
    1.25 -     realpow_0   "r ^ 0       = #1"
    1.26 -     realpow_Suc "r ^ (Suc n) = (r::real) * (r ^ n)"
    1.27 +     realpow_0:   "r ^ 0       = #1"
    1.28 +     realpow_Suc: "r ^ (Suc n) = (r::real) * (r ^ n)"
    1.29  
    1.30  end