changeset 5078 | 7b5ea59c0275 |
child 5588 | a3ab526bb891 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/Real/RealAbs.thy Thu Jun 25 13:57:34 1998 +0200 @@ -0,0 +1,13 @@ +(* Title : RealAbs.thy + Author : Jacques D. Fleuriot + Copyright : 1998 University of Cambridge + Description : Absolute value function for the reals +*) + +RealAbs = Real + + +constdefs + rabs :: real => real + "rabs r == if 0r<=r then r else %~r" + +end \ No newline at end of file