equal
deleted
inserted
replaced
88 end; |
88 end; |
89 |
89 |
90 |
90 |
91 (*****************************************************************************) |
91 (*****************************************************************************) |
92 (** Simplifying: **) |
92 (** Simplifying: **) |
93 (** Some useful lemmata, lists and simplification tactics to control which **) |
93 (** SOME useful lemmata, lists and simplification tactics to control which **) |
94 (** theorems are used to simplify at each moment, so that the original **) |
94 (** theorems are used to simplify at each moment, so that the original **) |
95 (** input does not suffer any unexpected transformation **) |
95 (** input does not suffer any unexpected transformation **) |
96 (*****************************************************************************) |
96 (*****************************************************************************) |
97 |
97 |
98 Goal "-(Collect b) = {x. ~(b x)}"; |
98 Goal "-(Collect b) = {x. ~(b x)}"; |