Rationalized the rewriting of membership for {} and insert
authorpaulson
Wed Sep 25 11:14:18 1996 +0200 (1996-09-25)
changeset 2024909153d8318f
parent 2023 aa25f20c5d8b
child 2025 9acc10ac1e1d
Rationalized the rewriting of membership for {} and insert
by deleting the redundant theorems in_empty and in_insert
src/HOL/Set.ML
src/HOL/equalities.ML
     1.1 --- a/src/HOL/Set.ML	Wed Sep 25 11:10:31 1996 +0200
     1.2 +++ b/src/HOL/Set.ML	Wed Sep 25 11:14:18 1996 +0200
     1.3 @@ -501,8 +501,8 @@
     1.4  (*** Set reasoning tools ***)
     1.5  
     1.6  
     1.7 -val mem_simps = [ Un_iff, Int_iff, Compl_iff, Diff_iff, singleton_iff,
     1.8 -		  mem_Collect_eq];
     1.9 +val mem_simps = [insert_iff, empty_iff, Un_iff, Int_iff, Compl_iff, Diff_iff, 
    1.10 +		 mem_Collect_eq];
    1.11  
    1.12  (*Not for Addsimps -- it can cause goals to blow up!*)
    1.13  goal Set.thy "(a : (if Q then x else y)) = ((Q --> a:x) & (~Q --> a : y))";
     2.1 --- a/src/HOL/equalities.ML	Wed Sep 25 11:10:31 1996 +0200
     2.2 +++ b/src/HOL/equalities.ML	Wed Sep 25 11:14:18 1996 +0200
     2.3 @@ -22,18 +22,6 @@
     2.4  qed "subset_empty";
     2.5  Addsimps [subset_empty];
     2.6  
     2.7 -section ":";
     2.8 -
     2.9 -goal Set.thy "x ~: {}";
    2.10 -by (Fast_tac 1);
    2.11 -qed "in_empty";
    2.12 -Addsimps[in_empty];
    2.13 -
    2.14 -goal Set.thy "x : insert y A = (x=y | x:A)";
    2.15 -by (Fast_tac 1);
    2.16 -qed "in_insert";
    2.17 -Addsimps[in_insert];
    2.18 -
    2.19  section "insert";
    2.20  
    2.21  (*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)