1
(* Title : RealAbs.thy
2
Author : Jacques D. Fleuriot
3
Copyright : 1998 University of Cambridge
4
Description : Absolute value function for the reals
5
*)
6
7
RealAbs = Real +
8
9
constdefs
10
rabs :: real => real
11
"rabs r == if 0r<=r then r else -r"
12
13
end