| changeset 10648 | a8c647cfa31f |
| parent 10606 | e3229a37d53f |
| child 10752 | c4f1bf2acf4c |
| 10647:a4529a251b6f | 10648:a8c647cfa31f |
|---|---|
35 |
35 |
36 real_diff_def |
36 real_diff_def |
37 "R - (S::real) == R + - S" |
37 "R - (S::real) == R + - S" |
38 |
38 |
39 real_inverse_def |
39 real_inverse_def |
40 "inverse (R::real) == (@S. R ~= 0 & S*R = 1r)" |
40 "inverse (R::real) == (SOME S. (R = 0 & S = 0) | S * R = 1r)" |
41 |
41 |
42 real_divide_def |
42 real_divide_def |
43 "R / (S::real) == R * inverse S" |
43 "R / (S::real) == R * inverse S" |
44 |
44 |
45 constdefs |
45 constdefs |