| changeset 59871 | e1a49ac9c537 |
| parent 58889 | 5b7a9633cfa8 |
| child 61343 | 5b5656a63bd6 |
| 59870:68d6b6aa4450 | 59871:e1a49ac9c537 |
|---|---|
76 apply simp oops |
76 apply simp oops |
77 |
77 |
78 lemma "- (2*i) + 3 + (2*i + 4) = (0::int)" |
78 lemma "- (2*i) + 3 + (2*i + 4) = (0::int)" |
79 apply simp oops |
79 apply simp oops |
80 |
80 |
81 (*Tobias's example dated 2015-03-02*) |
|
82 lemma "(pi * (real u * 2) = pi * (real (xa v) * - 2))" |
|
83 apply simp oops |
|
81 |
84 |
82 |
85 |
83 subsection {* Arithmetic Method Tests *} |
86 subsection {* Arithmetic Method Tests *} |
84 |
87 |
85 |
88 |