equal
deleted
inserted
replaced
549 qed "Union_image_eq"; |
549 qed "Union_image_eq"; |
550 Addsimps [Union_image_eq]; |
550 Addsimps [Union_image_eq]; |
551 |
551 |
552 Goal "f `` Union S = (UN x:S. f `` x)"; |
552 Goal "f `` Union S = (UN x:S. f `` x)"; |
553 by (Blast_tac 1); |
553 by (Blast_tac 1); |
554 qed "image_Union_eq"; |
554 qed "image_Union"; |
555 |
555 |
556 Goal "Inter(B``A) = (INT x:A. B(x))"; |
556 Goal "Inter(B``A) = (INT x:A. B(x))"; |
557 by (Blast_tac 1); |
557 by (Blast_tac 1); |
558 qed "Inter_image_eq"; |
558 qed "Inter_image_eq"; |
559 Addsimps [Inter_image_eq]; |
559 Addsimps [Inter_image_eq]; |