equal
deleted
inserted
replaced
290 unfolding iff_def |
290 unfolding iff_def |
291 apply (assumption | rule assms conjI impI)+ |
291 apply (assumption | rule assms conjI impI)+ |
292 done |
292 done |
293 |
293 |
294 |
294 |
295 (*Observe use of rewrite_rule to unfold "<->" in meta-assumptions (prems) *) |
|
296 |
|
297 schematic_lemma iffE: |
295 schematic_lemma iffE: |
298 assumes "p:P <-> Q" |
296 assumes "p:P <-> Q" |
299 and "!!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R" |
297 and "!!x y.[| x:P-->Q; y:Q-->P |] ==> q(x,y):R" |
300 shows "?p:R" |
298 shows "?p:R" |
301 apply (rule conjE) |
299 apply (rule conjE) |