changed deps;
authorwenzelm
Mon Jul 24 23:59:32 2000 +0200 (2000-07-24)
changeset 94298ebc549e9326
parent 9428 c8eb573114de
child 9430 c2dd2780f88d
changed deps;
src/HOL/Real/RComplete.thy
src/HOL/Real/RealAbs.thy
     1.1 --- a/src/HOL/Real/RComplete.thy	Mon Jul 24 23:59:08 2000 +0200
     1.2 +++ b/src/HOL/Real/RComplete.thy	Mon Jul 24 23:59:32 2000 +0200
     1.3 @@ -6,5 +6,5 @@
     1.4                    reals and reals 
     1.5  *) 
     1.6  
     1.7 -RComplete = Lubs + RealBin
     1.8 +RComplete = Lubs + RealArith
     1.9  
     2.1 --- a/src/HOL/Real/RealAbs.thy	Mon Jul 24 23:59:08 2000 +0200
     2.2 +++ b/src/HOL/Real/RealAbs.thy	Mon Jul 24 23:59:32 2000 +0200
     2.3 @@ -5,7 +5,7 @@
     2.4      Description : Absolute value function for the reals
     2.5  *) 
     2.6  
     2.7 -RealAbs = RealBin +
     2.8 +RealAbs = RealArith +
     2.9  
    2.10  
    2.11  defs