| changeset 5632 | 5682dce02591 |
| parent 5590 | 477fc12adceb |
| child 5762 | 149d435aa4d7 |
--- a/src/HOL/equalities.ML Fri Oct 09 11:25:26 1998 +0200 +++ b/src/HOL/equalities.ML Fri Oct 09 11:27:11 1998 +0200 @@ -706,6 +706,11 @@ by (Blast_tac 1); qed "Diff_Int_distrib2"; +Goal "A - - B = A Int B"; +by Auto_tac; +qed "Diff_Compl"; +Addsimps [Diff_Compl]; + section "Quantification over type \"bool\"";