src/HOL/HOLCF/ex/Powerdomain_ex.thy
changeset 41399 ad093e4638e2
parent 40774 0437dbc127b3
child 42151 4da4fc77664b
     1.1 --- a/src/HOL/HOLCF/ex/Powerdomain_ex.thy	Thu Dec 23 12:20:09 2010 +0100
     1.2 +++ b/src/HOL/HOLCF/ex/Powerdomain_ex.thy	Thu Dec 23 11:51:59 2010 -0800
     1.3 @@ -62,7 +62,7 @@
     1.4    pick :: "'a tree \<rightarrow> 'a convex_pd"
     1.5  where
     1.6    pick_Leaf: "pick\<cdot>(Leaf\<cdot>a) = {a}\<natural>"
     1.7 -| pick_Node: "pick\<cdot>(Node\<cdot>l\<cdot>r) = pick\<cdot>l +\<natural> pick\<cdot>r"
     1.8 +| pick_Node: "pick\<cdot>(Node\<cdot>l\<cdot>r) = pick\<cdot>l \<union>\<natural> pick\<cdot>r"
     1.9  
    1.10  lemma pick_strict [simp]: "pick\<cdot>\<bottom> = \<bottom>"
    1.11  by fixrec_simp