| changeset 25927 | 9c544dac6269 |
| parent 25925 | 3dc4acca4388 |
| child 27185 | 0407630909ef |
--- a/src/HOLCF/Fix.thy Fri Jan 18 20:31:11 2008 +0100 +++ b/src/HOLCF/Fix.thy Fri Jan 18 20:34:28 2008 +0100 @@ -59,7 +59,7 @@ "_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3FIX _./ _)" [1000, 10] 10) syntax (xsymbols) - "_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3\<mu>_./ _)" [1000, 10] 10) + "_FIX" :: "['a, 'a] \<Rightarrow> 'a" ("(3\<mu> _./ _)" [1000, 10] 10) translations "\<mu> x. t" == "CONST fix\<cdot>(\<Lambda> x. t)"