src/HOL/Hyperreal/HRealAbs.thy
author kleing
Tue, 13 May 2003 08:59:21 +0200
changeset 14024 213dcc39358f
parent 10919 144ede948e58
child 14269 502a7c95de73
permissions -rw-r--r--
HOL-Real -> HOL-Complex

(*  Title       : HRealAbs.thy
    Author      : Jacques D. Fleuriot
    Copyright   : 1998  University of Cambridge
    Description : Absolute value function for the hyperreals
*) 

HRealAbs = HyperArith + RealAbs + 

defs
    hrabs_def "abs r  == if (0::hypreal) <=r then r else -r" 

constdefs
  
  hypreal_of_nat :: nat => hypreal                   
  "hypreal_of_nat (n::nat) == hypreal_of_real (real n)"

end