src/HOL/Set.thy
changeset 46882 6242b4bc05bc
parent 46853 998ec26044c4
child 47398 07bcf80391d0
     1.1 --- a/src/HOL/Set.thy	Sun Mar 11 22:06:13 2012 +0100
     1.2 +++ b/src/HOL/Set.thy	Mon Mar 12 15:11:24 2012 +0100
     1.3 @@ -124,7 +124,8 @@
     1.4  qed (simp_all add: less_eq_set_def less_set_def inf_set_def sup_set_def
     1.5    bot_set_def top_set_def uminus_set_def minus_set_def
     1.6    less_le_not_le inf_compl_bot sup_compl_top sup_inf_distrib1 diff_eq
     1.7 -  set_eqI fun_eq_iff)
     1.8 +  set_eqI fun_eq_iff
     1.9 +  del: inf_apply sup_apply bot_apply top_apply minus_apply uminus_apply)
    1.10  
    1.11  end
    1.12