| changeset 9608 | a50dcf0475ad |
| parent 9447 | e5180c869772 |
| child 9969 | 4753185f1dd2 |
--- a/src/HOL/equalities.ML Mon Aug 14 18:49:35 2000 +0200 +++ b/src/HOL/equalities.ML Wed Aug 16 10:22:41 2000 +0200 @@ -795,6 +795,11 @@ qed "Diff_Compl"; Addsimps [Diff_Compl]; +Goal "- (A-B) = -A Un B"; +by (blast_tac (claset() addIs []) 1); +qed "Compl_Diff_eq"; +Addsimps [Compl_Diff_eq]; + section "Quantification over type \"bool\"";