# HG changeset patch
# User huffman
# Date 1267499888 28800
# Node ID 5d200f2d7a4fd35961c3923cb6332ec8dbc61218
# Parent  92e0028a46f2dca8433ab88bee41ce728df4a434
add lemma lub_eq

diff -r 92e0028a46f2 -r 5d200f2d7a4f src/HOLCF/Pcpo.thy
--- a/src/HOLCF/Pcpo.thy	Mon Mar 01 17:32:23 2010 -0800
+++ b/src/HOLCF/Pcpo.thy	Mon Mar 01 19:18:08 2010 -0800
@@ -91,6 +91,10 @@
     \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
   by (simp only: expand_fun_eq [symmetric])
 
+lemma lub_eq:
+  "(\<And>i. X i = Y i) \<Longrightarrow> (\<Squnion>i. X i) = (\<Squnion>i. Y i)"
+  by simp
+
 text {* more results about mono and = of lubs of chains *}
 
 lemma lub_mono2: