| changeset 10750 | a681d3df1a39 |
| child 10778 | 2c6605049646 |
| 10749:afdb47b97317 | 10750:a681d3df1a39 |
|---|---|
1 (* Title : HRealAbs.thy |
|
2 Author : Jacques D. Fleuriot |
|
3 Copyright : 1998 University of Cambridge |
|
4 Description : Absolute value function for the hyperreals |
|
5 *) |
|
6 |
|
7 HRealAbs = HyperArith + RealAbs + |
|
8 |
|
9 defs |
|
10 hrabs_def "abs r == if (0::hypreal) <=r then r else -r" |
|
11 |
|
12 end |