src/HOL/equalities.ML
changeset 1264 3eb91524b938
parent 1179 7678408f9751
child 1465 5d7a7e439cec
     1.1 --- a/src/HOL/equalities.ML	Wed Oct 04 13:01:05 1995 +0100
     1.2 +++ b/src/HOL/equalities.ML	Wed Oct 04 13:10:03 1995 +0100
     1.3 @@ -337,7 +337,7 @@
     1.4  by (fast_tac eq_cs 1);
     1.5  qed "Diff_Int";
     1.6  
     1.7 -val set_ss = set_ss addsimps
     1.8 +Addsimps
     1.9    [in_empty,in_insert,insert_subset,
    1.10     insert_not_empty,empty_not_insert,
    1.11     Int_absorb,Int_empty_left,Int_empty_right,