equal
deleted
inserted
replaced
703 qed "Diff_Int_distrib"; |
703 qed "Diff_Int_distrib"; |
704 |
704 |
705 Goal "(A-B) Int C = (A Int C) - (B Int C)"; |
705 Goal "(A-B) Int C = (A Int C) - (B Int C)"; |
706 by (Blast_tac 1); |
706 by (Blast_tac 1); |
707 qed "Diff_Int_distrib2"; |
707 qed "Diff_Int_distrib2"; |
|
708 |
|
709 Goal "A - - B = A Int B"; |
|
710 by Auto_tac; |
|
711 qed "Diff_Compl"; |
|
712 Addsimps [Diff_Compl]; |
708 |
713 |
709 |
714 |
710 section "Quantification over type \"bool\""; |
715 section "Quantification over type \"bool\""; |
711 |
716 |
712 Goal "(ALL b::bool. P b) = (P True & P False)"; |
717 Goal "(ALL b::bool. P b) = (P True & P False)"; |