--- a/src/HOL/HOLCF/Deflation.thy Wed Dec 15 20:52:20 2010 +0100
+++ b/src/HOL/HOLCF/Deflation.thy Wed Dec 15 19:15:06 2010 -0800
@@ -206,18 +206,18 @@
lemma compact_e_rev: "compact (e\<cdot>x) \<Longrightarrow> compact x"
proof -
assume "compact (e\<cdot>x)"
- hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (rule compactD)
- hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
- hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by simp
+ hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> y)" by (rule compactD)
+ hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> e\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
+ hence "adm (\<lambda>y. x \<notsqsubseteq> y)" by simp
thus "compact x" by (rule compactI)
qed
lemma compact_e: "compact x \<Longrightarrow> compact (e\<cdot>x)"
proof -
assume "compact x"
- hence "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" by (rule compactD)
- hence "adm (\<lambda>y. \<not> x \<sqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
- hence "adm (\<lambda>y. \<not> e\<cdot>x \<sqsubseteq> y)" by (simp add: e_below_iff_below_p)
+ hence "adm (\<lambda>y. x \<notsqsubseteq> y)" by (rule compactD)
+ hence "adm (\<lambda>y. x \<notsqsubseteq> p\<cdot>y)" by (rule adm_subst [OF cont_Rep_cfun2])
+ hence "adm (\<lambda>y. e\<cdot>x \<notsqsubseteq> y)" by (simp add: e_below_iff_below_p)
thus "compact (e\<cdot>x)" by (rule compactI)
qed