equal
deleted
inserted
replaced
7 |
7 |
8 RealAbs = RealArith + |
8 RealAbs = RealArith + |
9 |
9 |
10 |
10 |
11 defs |
11 defs |
12 real_abs_def "abs r == (if (Numeral0::real) <= r then r else -r)" |
12 real_abs_def "abs r == (if (0::real) <= r then r else -r)" |
13 |
13 |
14 end |
14 end |