changeset 35115 | 446c5063e4fd |
parent 33808 | 31169fdc5ae7 |
child 35427 | ad039d29e01c |
child 35491 | 92e0028a46f2 |
--- a/src/HOLCF/Sprod.thy Thu Feb 11 22:55:16 2010 +0100 +++ b/src/HOLCF/Sprod.thy Thu Feb 11 23:00:22 2010 +0100 @@ -51,7 +51,7 @@ "ssplit = (\<Lambda> f. strictify\<cdot>(\<Lambda> p. f\<cdot>(sfst\<cdot>p)\<cdot>(ssnd\<cdot>p)))" syntax - "@stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))") + "_stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))") translations "(:x, y, z:)" == "(:x, (:y, z:):)" "(:x, y:)" == "CONST spair\<cdot>x\<cdot>y"