src/HOL/HOLCF/Porder.thy
changeset 41182 717404c7d59a
parent 40774 0437dbc127b3
child 42151 4da4fc77664b
     1.1 --- a/src/HOL/HOLCF/Porder.thy	Wed Dec 15 20:52:20 2010 +0100
     1.2 +++ b/src/HOL/HOLCF/Porder.thy	Wed Dec 15 19:15:06 2010 -0800
     1.3 @@ -20,6 +20,13 @@
     1.4  notation (xsymbols)
     1.5    below (infix "\<sqsubseteq>" 50)
     1.6  
     1.7 +abbreviation
     1.8 +  not_below :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infix "~<<" 50)
     1.9 +  where "not_below x y \<equiv> \<not> below x y"
    1.10 +
    1.11 +notation (xsymbols)
    1.12 +  not_below (infix "\<notsqsubseteq>" 50)
    1.13 +
    1.14  lemma below_eq_trans: "\<lbrakk>a \<sqsubseteq> b; b = c\<rbrakk> \<Longrightarrow> a \<sqsubseteq> c"
    1.15    by (rule subst)
    1.16  
    1.17 @@ -46,7 +53,7 @@
    1.18  lemma rev_below_trans: "y \<sqsubseteq> z \<Longrightarrow> x \<sqsubseteq> y \<Longrightarrow> x \<sqsubseteq> z"
    1.19    by (rule below_trans)
    1.20  
    1.21 -lemma not_below2not_eq: "\<not> x \<sqsubseteq> y \<Longrightarrow> x \<noteq> y"
    1.22 +lemma not_below2not_eq: "x \<notsqsubseteq> y \<Longrightarrow> x \<noteq> y"
    1.23    by auto
    1.24  
    1.25  end