src/HOL/HOLCF/Domain.thy
changeset 67399 eab6ce8368fa
parent 63432 ba7901e94e7b
child 68357 6bf71e776226
     1.1 --- a/src/HOL/HOLCF/Domain.thy	Wed Jan 10 15:21:49 2018 +0100
     1.2 +++ b/src/HOL/HOLCF/Domain.thy	Wed Jan 10 15:25:09 2018 +0100
     1.3 @@ -97,7 +97,7 @@
     1.4    fixes Abs :: "udom \<Rightarrow> 'a::pcpo"
     1.5    fixes t :: "udom defl"
     1.6    assumes type: "type_definition Rep Abs (defl_set t)"
     1.7 -  assumes below: "op \<sqsubseteq> \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     1.8 +  assumes below: "(\<sqsubseteq>) \<equiv> \<lambda>x y. Rep x \<sqsubseteq> Rep y"
     1.9    assumes emb: "emb \<equiv> (\<Lambda> x. Rep x)"
    1.10    assumes prj: "prj \<equiv> (\<Lambda> x. Abs (cast\<cdot>t\<cdot>x))"
    1.11    assumes defl: "defl \<equiv> (\<lambda> a::'a itself. t)"