changeset 10574 | 8f98f0301d67 |
parent 9436 | 62bb04ab4b01 |
child 10648 | a8c647cfa31f |
10573:1751ab881289 | 10574:8f98f0301d67 |
---|---|
1 |
|
2 (*useful??*) |
1 (*useful??*) |
3 Goal "(z = z + w) = (w = (#0::real))"; |
2 Goal "(z = z + w) = (w = (#0::real))"; |
4 by Auto_tac; |
3 by Auto_tac; |
5 qed "real_add_left_cancel0"; |
4 qed "real_add_left_cancel0"; |
6 Addsimps [real_add_left_cancel0]; |
5 Addsimps [real_add_left_cancel0]; |