equal
deleted
inserted
replaced
459 using a |
459 using a |
460 apply (metis COMBC_def Collect_def Collect_mem_eq a) |
460 apply (metis COMBC_def Collect_def Collect_mem_eq a) |
461 done |
461 done |
462 |
462 |
463 lemma RIGHT_RES_FORALL_REGULAR: |
463 lemma RIGHT_RES_FORALL_REGULAR: |
464 assumes a: "!x :: 'a. (R x --> P x --> Q x)" |
464 assumes a: "\<And>x :: 'a. (R x \<Longrightarrow> P x \<longrightarrow> Q x)" |
465 shows "All P ==> Ball R Q" |
465 shows "All P \<longrightarrow> Ball R Q" |
466 using a |
466 using a |
467 apply (metis COMBC_def Collect_def Collect_mem_eq a) |
467 apply (metis COMBC_def Collect_def Collect_mem_eq a) |
468 done |
468 done |
469 |
469 |
470 lemma LEFT_RES_EXISTS_REGULAR: |
470 lemma LEFT_RES_EXISTS_REGULAR: |