equal
deleted
inserted
replaced
169 |
169 |
170 lemmas [sym] = sym iff_sym not_sym iff_not_sym |
170 lemmas [sym] = sym iff_sym not_sym iff_not_sym |
171 and [Pure.elim?] = iffD1 iffD2 impE |
171 and [Pure.elim?] = iffD1 iffD2 impE |
172 |
172 |
173 |
173 |
|
174 lemma eq_commute: "a=b <-> b=a" |
|
175 apply (rule iffI) |
|
176 apply (erule sym)+ |
|
177 done |
|
178 |
|
179 |
174 subsection {* Atomizing meta-level rules *} |
180 subsection {* Atomizing meta-level rules *} |
175 |
181 |
176 lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" |
182 lemma atomize_all [atomize]: "(!!x. P(x)) == Trueprop (ALL x. P(x))" |
177 proof |
183 proof |
178 assume "!!x. P(x)" |
184 assume "!!x. P(x)" |