equal
deleted
inserted
replaced
45 FIXME: we should have this, as for type int, but many proofs would break. |
45 FIXME: we should have this, as for type int, but many proofs would break. |
46 It replaces x+-y by x-y. |
46 It replaces x+-y by x-y. |
47 Addsimps [symmetric real_diff_def] |
47 Addsimps [symmetric real_diff_def] |
48 *) |
48 *) |
49 |
49 |
50 (** Division by 1, -1 **) |
50 subsubsection{*Division By @{term 1} and @{term "-1"}*} |
51 |
51 |
52 lemma real_divide_minus1 [simp]: "x/-1 = -(x::real)" |
52 lemma real_divide_minus1 [simp]: "x/-1 = -(x::real)" |
53 by simp |
53 by simp |
54 |
54 |
55 lemma real_minus1_divide [simp]: "-1/(x::real) = - (1/x)" |
55 lemma real_minus1_divide [simp]: "-1/(x::real) = - (1/x)" |