src/HOL/HOLCF/Domain_Aux.thy
changeset 41182 717404c7d59a
parent 40774 0437dbc127b3
child 41430 1aa23e9f2c87
     1.1 --- a/src/HOL/HOLCF/Domain_Aux.thy	Wed Dec 15 20:52:20 2010 +0100
     1.2 +++ b/src/HOL/HOLCF/Domain_Aux.thy	Wed Dec 15 19:15:06 2010 -0800
     1.3 @@ -86,10 +86,10 @@
     1.4  
     1.5  lemma compact_abs_rev: "compact (abs\<cdot>x) \<Longrightarrow> compact x"
     1.6  proof (unfold compact_def)
     1.7 -  assume "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> y)"
     1.8 +  assume "adm (\<lambda>y. abs\<cdot>x \<notsqsubseteq> y)"
     1.9    with cont_Rep_cfun2
    1.10 -  have "adm (\<lambda>y. \<not> abs\<cdot>x \<sqsubseteq> abs\<cdot>y)" by (rule adm_subst)
    1.11 -  then show "adm (\<lambda>y. \<not> x \<sqsubseteq> y)" using abs_below by simp
    1.12 +  have "adm (\<lambda>y. abs\<cdot>x \<notsqsubseteq> abs\<cdot>y)" by (rule adm_subst)
    1.13 +  then show "adm (\<lambda>y. x \<notsqsubseteq> y)" using abs_below by simp
    1.14  qed
    1.15  
    1.16  lemma compact_rep_rev: "compact (rep\<cdot>x) \<Longrightarrow> compact x"