| changeset 20770 | 2c583720436e |
| parent 19621 | 475140eb82f2 |
| child 21524 | 7843e2fd14a9 |
--- a/src/HOLCF/Porder.thy Thu Sep 28 23:42:39 2006 +0200 +++ b/src/HOLCF/Porder.thy Thu Sep 28 23:42:43 2006 +0200 @@ -94,7 +94,7 @@ "LUB " :: "[idts, 'a] \<Rightarrow> 'a" ("(3\<Squnion>_./ _)" [0,10] 10) translations - "\<Squnion>n. t" == "lub(range(\<lambda>n. t))" + "\<Squnion>n. t" == "lub(CONST range(\<lambda>n. t))" text {* lubs are unique *}