On Wed, 21 Sep 2011, Brian Huffman wrote:
On Tue, Sep 20, 2011 at 10:03 AM, Christian Urban <urb...@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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
