# HG changeset patch
# User huffman
# Date 1118266999 -7200
# Node ID 50a613925c4eedebca39a669ff17720a246ced73
# Parent  a6431098a92971fe8d791e1a163524c2f5bdfb82
make up_eq and up_less into simp rules

diff -r a6431098a929 -r 50a613925c4e src/HOLCF/Up.thy
--- a/src/HOLCF/Up.thy	Wed Jun 08 16:11:09 2005 +0200
+++ b/src/HOLCF/Up.thy	Wed Jun 08 23:43:19 2005 +0200
@@ -285,7 +285,7 @@
 lemma up_inject: "up\<cdot>x = up\<cdot>y \<Longrightarrow> x = y"
 by (simp add: up_def cont_Iup)
 
-lemma up_eq: "(up\<cdot>x = up\<cdot>y) = (x = y)"
+lemma up_eq [simp]: "(up\<cdot>x = up\<cdot>y) = (x = y)"
 by (rule iffI, erule up_inject, simp)
 
 lemma up_defined [simp]: " up\<cdot>x \<noteq> \<bottom>"
@@ -294,7 +294,7 @@
 lemma not_up_less_UU [simp]: "\<not> up\<cdot>x \<sqsubseteq> \<bottom>"
 by (simp add: eq_UU_iff [symmetric])
 
-lemma up_less: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
+lemma up_less [simp]: "(up\<cdot>x \<sqsubseteq> up\<cdot>y) = (x \<sqsubseteq> y)"
 by (simp add: up_def cont_Iup)
 
 lemma upE1: "\<lbrakk>p = \<bottom> \<Longrightarrow> Q; \<And>x. p = up\<cdot>x \<Longrightarrow> Q\<rbrakk> \<Longrightarrow> Q"