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/cprod1.thy
ID: $Id$
Author: Franz Regensburger
Copyright 1993 Technische Universitaet Muenchen
Partial ordering for cartesian product of HOL theory prod.thy
*)
Cprod1 = Cfun3 +
consts
less_cprod :: "[('a::pcpo * 'b::pcpo),('a * 'b)] => bool"
rules
less_cprod_def "less_cprod(p1,p2) == ( fst(p1) << fst(p2) &\
\ snd(p1) << snd(p2))"
end