| changeset 10778 | 2c6605049646 |
| parent 10750 | a681d3df1a39 |
| child 10919 | 144ede948e58 |
| 10777:a5a6255748c3 | 10778:2c6605049646 |
|---|---|
7 HRealAbs = HyperArith + RealAbs + |
7 HRealAbs = HyperArith + RealAbs + |
8 |
8 |
9 defs |
9 defs |
10 hrabs_def "abs r == if (0::hypreal) <=r then r else -r" |
10 hrabs_def "abs r == if (0::hypreal) <=r then r else -r" |
11 |
11 |
12 constdefs |
|
13 |
|
14 hypreal_of_nat :: nat => hypreal |
|
15 "hypreal_of_nat n == hypreal_of_real (real_of_nat n)" |
|
16 |
|
12 end |
17 end |