equal
deleted
inserted
replaced
222 apply (erule impI) |
222 apply (erule impI) |
223 apply (erule impI) |
223 apply (erule impI) |
224 done |
224 done |
225 |
225 |
226 |
226 |
227 (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *) |
|
228 lemma iffE: |
227 lemma iffE: |
229 assumes major: "P <-> Q" |
228 assumes major: "P <-> Q" |
230 and r: "P-->Q ==> Q-->P ==> R" |
229 and r: "P-->Q ==> Q-->P ==> R" |
231 shows R |
230 shows R |
232 apply (insert major, unfold iff_def) |
231 apply (insert major, unfold iff_def) |