| author | wenzelm |
| Mon, 09 Dec 1996 16:38:28 +0100 | |
| changeset 2344 | c3e1eaea4418 |
| parent 1479 | 21eb5e156d91 |
| child 2640 | ee4dfce170a0 |
| permissions | -rw-r--r-- |
(* Title: HOLCF/cprod2.thy ID: $Id$ Author: Franz Regensburger Copyright 1993 Technische Universitaet Muenchen Class Instance *::(pcpo,pcpo)po *) Cprod2 = Cprod1 + (* Witness for the above arity axiom is cprod1.ML *) arities "*" :: (pcpo,pcpo)po rules (* instance of << for type ['a * 'b] *) inst_cprod_po "((op <<)::['a * 'b,'a * 'b]=>bool) = less_cprod" end