changeset 41479 | 655f583840d0 |
parent 41430 | 1aa23e9f2c87 |
child 42151 | 4da4fc77664b |
--- a/src/HOL/HOLCF/ConvexPD.thy Sat Jan 08 10:02:43 2011 -0800 +++ b/src/HOL/HOLCF/ConvexPD.thy Sat Jan 08 11:18:09 2011 -0800 @@ -181,7 +181,7 @@ "xs \<union>\<natural> ys == convex_plus\<cdot>xs\<cdot>ys" syntax - "_convex_pd" :: "args \<Rightarrow> 'a convex_pd" ("{_}\<natural>") + "_convex_pd" :: "args \<Rightarrow> logic" ("{_}\<natural>") translations "{x,xs}\<natural>" == "{x}\<natural> \<union>\<natural> {xs}\<natural>"