src/HOL/HOLCF/Tr.thy
changeset 41182 717404c7d59a
parent 40774 0437dbc127b3
child 41295 5b5388d4ccc9
     1.1 --- a/src/HOL/HOLCF/Tr.thy	Wed Dec 15 20:52:20 2010 +0100
     1.2 +++ b/src/HOL/HOLCF/Tr.thy	Wed Dec 15 19:15:06 2010 -0800
     1.3 @@ -40,7 +40,7 @@
     1.4  text {* distinctness for type @{typ tr} *}
     1.5  
     1.6  lemma dist_below_tr [simp]:
     1.7 -  "\<not> TT \<sqsubseteq> \<bottom>" "\<not> FF \<sqsubseteq> \<bottom>" "\<not> TT \<sqsubseteq> FF" "\<not> FF \<sqsubseteq> TT"
     1.8 +  "TT \<notsqsubseteq> \<bottom>" "FF \<notsqsubseteq> \<bottom>" "TT \<notsqsubseteq> FF" "FF \<notsqsubseteq> TT"
     1.9  unfolding TT_def FF_def by simp_all
    1.10  
    1.11  lemma dist_eq_tr [simp]:
    1.12 @@ -53,10 +53,10 @@
    1.13  lemma FF_below_iff [simp]: "FF \<sqsubseteq> x \<longleftrightarrow> x = FF"
    1.14  by (induct x rule: tr_induct) simp_all
    1.15  
    1.16 -lemma not_below_TT_iff [simp]: "\<not> (x \<sqsubseteq> TT) \<longleftrightarrow> x = FF"
    1.17 +lemma not_below_TT_iff [simp]: "x \<notsqsubseteq> TT \<longleftrightarrow> x = FF"
    1.18  by (induct x rule: tr_induct) simp_all
    1.19  
    1.20 -lemma not_below_FF_iff [simp]: "\<not> (x \<sqsubseteq> FF) \<longleftrightarrow> x = TT"
    1.21 +lemma not_below_FF_iff [simp]: "x \<notsqsubseteq> FF \<longleftrightarrow> x = TT"
    1.22  by (induct x rule: tr_induct) simp_all
    1.23  
    1.24