src/HOL/Set.thy
changeset 44490 e3e8d20a6ebc
parent 44241 7943b69f0188
child 44744 bdf8eb8f126b
equal deleted inserted replaced
44489:6cddca146ca0 44490:e3e8d20a6ebc
  1375 lemma Compl_subset_Compl_iff [iff]: "(-A \<subseteq> -B) = (B \<subseteq> A)"
  1375 lemma Compl_subset_Compl_iff [iff]: "(-A \<subseteq> -B) = (B \<subseteq> A)"
  1376   by (fact compl_le_compl_iff)
  1376   by (fact compl_le_compl_iff)
  1377 
  1377 
  1378 lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"
  1378 lemma Compl_eq_Compl_iff [iff]: "(-A = -B) = (A = (B::'a set))"
  1379   by (fact compl_eq_compl_iff)
  1379   by (fact compl_eq_compl_iff)
       
  1380 
       
  1381 lemma Compl_insert: "- insert x A = (-A) - {x}"
       
  1382   by blast
  1380 
  1383 
  1381 text {* \medskip Bounded quantifiers.
  1384 text {* \medskip Bounded quantifiers.
  1382 
  1385 
  1383   The following are not added to the default simpset because
  1386   The following are not added to the default simpset because
  1384   (a) they duplicate the body and (b) there are no similar rules for @{text Int}. *}
  1387   (a) they duplicate the body and (b) there are no similar rules for @{text Int}. *}