added print translations tha avoid eta contraction for important binders.
(* Title: HOLCF/sprod3.thy
ID: $Id$
Author: Franz Regensburger
License: GPL (GNU GENERAL PUBLIC LICENSE)
Class instance of ** for class pcpo
*)
Sprod3 = Sprod2 +
instance "**" :: (pcpo,pcpo)pcpo (least_sprod,cpo_sprod)
consts
spair :: "'a -> 'b -> ('a**'b)" (* continuous strict pairing *)
sfst :: "('a**'b)->'a"
ssnd :: "('a**'b)->'b"
ssplit :: "('a->'b->'c)->('a**'b)->'c"
syntax
"@stuple" :: "['a, args] => 'a ** 'b" ("(1'(:_,/ _:'))")
translations
"(:x, y, z:)" == "(:x, (:y, z:):)"
"(:x, y:)" == "spair$x$y"
defs
spair_def "spair == (LAM x y. Ispair x y)"
sfst_def "sfst == (LAM p. Isfst p)"
ssnd_def "ssnd == (LAM p. Issnd p)"
ssplit_def "ssplit == (LAM f. strictify$(LAM p. f$(sfst$p)$(ssnd$p)))"
end