domain package:
* theorems are stored in the theory
* creates hierachical name space
* minor changes to some names and values (for consistency),
e.g. cases -> casedist, dists_eq -> dist_eqs,
[take_lemma] -> take_lemmas
* separator between mutual domain definitions changed from "," to "and"
* minor debugging of Domain_Library.mk_var_names
(* Title: HOLCF/sprod3.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Class instance of ** for class pcpo
*)
Sprod3 = Sprod2 +
arities "**" :: (pcpo,pcpo)pcpo (* Witness sprod2.ML *)
consts
"@spair" :: "'a => 'b => ('a**'b)" ("_##_" [101,100] 100)
"cop @spair" :: "'a -> 'b -> ('a**'b)" ("spair")
(* continuous strict pairing *)
sfst :: "('a**'b)->'a"
ssnd :: "('a**'b)->'b"
ssplit :: "('a->'b->'c)->('a**'b)->'c"
rules
inst_sprod_pcpo "UU::'a**'b = Ispair(UU,UU)"
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
ML
(* ----------------------------------------------------------------------*)
(* parse translations for the above mixfix *)
(* ----------------------------------------------------------------------*)
val parse_translation = [("@spair",mk_cinfixtr "@spair")];