| changeset 5078 | 7b5ea59c0275 |
| child 5588 | a3ab526bb891 |
| 5077:71043526295f | 5078:7b5ea59c0275 |
|---|---|
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 |