[isabelle-dev] NEWS -> Redundant lemmas

[Johannes Hoelzl]

On Wed, 21 Sep 2011, Brian Huffman wrote:
> On Tue, Sep 20, 2011 at 10:03 AM, Christian Urban <urbanc at in.tum.de> wrote:
> I was able to put together replacement theorems for a few of these lemmas:
>
> Inf_singleton ~> Inf_insert [where A="{}", unfolded Inf_empty inf_top_right]
> Sup_singleton ~> Sup_insert [where A="{}", unfolded Sup_empty sup_bot_right]
> INTER_eq_Inter_image ~> INF_def
> UNION_eq_Union_image ~> SUP_def
> INF_subset ~> INF_superset_mono [OF _ order_refl]
>
[..]

I added this information to the NEWS entry.