src/HOL/equalities.ML
changeset 2024 909153d8318f
parent 2021 dd5866263153
child 2031 03a843f0f447
     1.1 --- a/src/HOL/equalities.ML	Wed Sep 25 11:10:31 1996 +0200
     1.2 +++ b/src/HOL/equalities.ML	Wed Sep 25 11:14:18 1996 +0200
     1.3 @@ -22,18 +22,6 @@
     1.4  qed "subset_empty";
     1.5  Addsimps [subset_empty];
     1.6  
     1.7 -section ":";
     1.8 -
     1.9 -goal Set.thy "x ~: {}";
    1.10 -by (Fast_tac 1);
    1.11 -qed "in_empty";
    1.12 -Addsimps[in_empty];
    1.13 -
    1.14 -goal Set.thy "x : insert y A = (x=y | x:A)";
    1.15 -by (Fast_tac 1);
    1.16 -qed "in_insert";
    1.17 -Addsimps[in_insert];
    1.18 -
    1.19  section "insert";
    1.20  
    1.21  (*NOT SUITABLE FOR REWRITING since {a} == insert a {}*)