equal
deleted
inserted
replaced
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}. *} 