| changeset 46125 | 00cd193a48dc |
| parent 42151 | 4da4fc77664b |
| child 58249 | 180f1b3508ed |
--- a/src/HOL/HOLCF/Up.thy Thu Jan 05 15:31:49 2012 +0100 +++ b/src/HOL/HOLCF/Up.thy Thu Jan 05 18:18:39 2012 +0100 @@ -181,6 +181,7 @@ translations "case l of XCONST up\<cdot>x \<Rightarrow> t" == "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l" + "case l of (XCONST up :: 'a)\<cdot>x \<Rightarrow> t" => "CONST fup\<cdot>(\<Lambda> x. t)\<cdot>l" "\<Lambda>(XCONST up\<cdot>x). t" == "CONST fup\<cdot>(\<Lambda> x. t)" text {* continuous versions of lemmas for @{typ "('a)u"} *}