src/HOL/Real/Hyperreal/HRealAbs.thy
changeset 10045 c76b73e16711
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Real/Hyperreal/HRealAbs.thy	Thu Sep 21 12:17:11 2000 +0200
     1.3 @@ -0,0 +1,12 @@
     1.4 +(*  Title       : HRealAbs.thy
     1.5 +    Author      : Jacques D. Fleuriot
     1.6 +    Copyright   : 1998  University of Cambridge
     1.7 +    Description : Absolute value function for the hyperreals
     1.8 +*) 
     1.9 +
    1.10 +HRealAbs = HyperOrd + RealAbs + 
    1.11 +
    1.12 +defs
    1.13 +    hrabs_def "abs r  == if (0::hypreal) <=r then r else -r" 
    1.14 +
    1.15 +end
    1.16 \ No newline at end of file