src/HOL/Set.thy
 changeset 44490 e3e8d20a6ebc parent 44241 7943b69f0188 child 44744 bdf8eb8f126b
equal 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}. *}`