--- a/src/HOL/HOLCF/Tr.thy Wed Dec 15 20:52:20 2010 +0100
+++ b/src/HOL/HOLCF/Tr.thy Wed Dec 15 19:15:06 2010 -0800
@@ -40,7 +40,7 @@
text {* distinctness for type @{typ tr} *}
lemma dist_below_tr [simp]:
- "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT"
+ "TT \<notsqsubseteq> \<bottom>" "FF \<notsqsubseteq> \<bottom>" "TT \<notsqsubseteq> FF" "FF \<notsqsubseteq> TT"
unfolding TT_def FF_def by simp_all
lemma dist_eq_tr [simp]:
@@ -53,10 +53,10 @@
lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
by (induct x rule: tr_induct) simp_all
-lemma not_below_TT_iff [simp]: "\<not> (x \<sqsubseteq> TT) \<longleftrightarrow> x = FF"
+lemma not_below_TT_iff [simp]: "x \<notsqsubseteq> TT \<longleftrightarrow> x = FF"
by (induct x rule: tr_induct) simp_all
-lemma not_below_FF_iff [simp]: "\<not> (x \<sqsubseteq> FF) \<longleftrightarrow> x = TT"
+lemma not_below_FF_iff [simp]: "x \<notsqsubseteq> FF \<longleftrightarrow> x = TT"
by (induct x rule: tr_induct) simp_all