| author | wenzelm |
| Wed, 24 Jul 2002 00:11:24 +0200 | |
| changeset 13413 | 0b60b9e18a26 |
| 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