author | kleing |
Tue, 13 May 2003 08:59:21 +0200 | |
changeset 14024 | 213dcc39358f |
parent 10919 | 144ede948e58 |
child 14269 | 502a7c95de73 |
permissions | -rw-r--r-- |
(* 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