equal
deleted
inserted
replaced
31 |
31 |
32 real_diff_def "x - y == x + -(y::real)" |
32 real_diff_def "x - y == x + -(y::real)" |
33 |
33 |
34 constdefs |
34 constdefs |
35 |
35 |
36 real_preal :: preal => real ("%#_" [80] 80) |
36 real_preal :: preal => real ("%#_" [100] 100) |
37 "%# m == Abs_real(realrel^^{(m+@#($#1p),@#($#1p))})" |
37 "%# m == Abs_real(realrel^^{(m+@#($#1p),@#($#1p))})" |
38 |
38 |
39 rinv :: real => real |
39 rinv :: real => real |
40 "rinv(R) == (@S. R ~= 0r & S*R = 1r)" |
40 "rinv(R) == (@S. R ~= 0r & S*R = 1r)" |
41 |
41 |
42 real_nat :: nat => real ("%%# _" [80] 80) |
42 real_nat :: nat => real ("%%# _" [100] 100) |
43 "%%# n == %#(@#($#(*# n)))" |
43 "%%# n == %#(@#($#(*# n)))" |
44 |
44 |
45 defs |
45 defs |
46 |
46 |
47 real_add_def |
47 real_add_def |