# HG changeset patch
# User huffman
# Date 1266423586 28800
# Node ID 07b3112e464b527693c69ecf2ec3132c4e563bf6
# Parent  eba22d68a0a7abcaeafcba2ec6028377785acd8d
fix warnings about duplicate simp rules

diff -r eba22d68a0a7 -r 07b3112e464b src/HOLCF/Cfun.thy
--- a/src/HOLCF/Cfun.thy	Wed Feb 17 08:05:16 2010 -0800
+++ b/src/HOLCF/Cfun.thy	Wed Feb 17 08:19:46 2010 -0800
@@ -521,7 +521,7 @@
 text {* results about strictify *}
 
 lemma cont_strictify1: "cont (\<lambda>f. if x = \<bottom> then \<bottom> else f\<cdot>x)"
-by (simp add: cont_if)
+by simp
 
 lemma monofun_strictify2: "monofun (\<lambda>x. if x = \<bottom> then \<bottom> else f\<cdot>x)"
 apply (rule monofunI)
diff -r eba22d68a0a7 -r 07b3112e464b src/HOLCF/Deflation.thy
--- a/src/HOLCF/Deflation.thy	Wed Feb 17 08:05:16 2010 -0800
+++ b/src/HOLCF/Deflation.thy	Wed Feb 17 08:19:46 2010 -0800
@@ -316,16 +316,14 @@
 subsection {* Uniqueness of ep-pairs *}
 
 lemma ep_pair_unique_e_lemma:
-  assumes "ep_pair e1 p" and "ep_pair e2 p"
+  assumes 1: "ep_pair e1 p" and 2: "ep_pair e2 p"
   shows "e1 \<sqsubseteq> e2"
 proof (rule below_cfun_ext)
-  interpret e1: ep_pair e1 p by fact
-  interpret e2: ep_pair e2 p by fact
   fix x
   have "e1\<cdot>(p\<cdot>(e2\<cdot>x)) \<sqsubseteq> e2\<cdot>x"
-    by (rule e1.e_p_below)
+    by (rule ep_pair.e_p_below [OF 1])
   thus "e1\<cdot>x \<sqsubseteq> e2\<cdot>x"
-    by (simp only: e2.e_inverse)
+    by (simp only: ep_pair.e_inverse [OF 2])
 qed
 
 lemma ep_pair_unique_e:
@@ -333,18 +331,16 @@
 by (fast intro: below_antisym elim: ep_pair_unique_e_lemma)
 
 lemma ep_pair_unique_p_lemma:
-  assumes "ep_pair e p1" and "ep_pair e p2"
+  assumes 1: "ep_pair e p1" and 2: "ep_pair e p2"
   shows "p1 \<sqsubseteq> p2"
 proof (rule below_cfun_ext)
-  interpret p1: ep_pair e p1 by fact
-  interpret p2: ep_pair e p2 by fact
   fix x
   have "e\<cdot>(p1\<cdot>x) \<sqsubseteq> x"
-    by (rule p1.e_p_below)
+    by (rule ep_pair.e_p_below [OF 1])
   hence "p2\<cdot>(e\<cdot>(p1\<cdot>x)) \<sqsubseteq> p2\<cdot>x"
     by (rule monofun_cfun_arg)
   thus "p1\<cdot>x \<sqsubseteq> p2\<cdot>x"
-    by (simp only: p2.e_inverse)
+    by (simp only: ep_pair.e_inverse [OF 2])
 qed
 
 lemma ep_pair_unique_p: