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