| author | wenzelm |
| Wed, 06 Aug 1997 14:42:44 +0200 | |
| changeset 3631 | 88a279998f90 |
| parent 243 | c22b85994e17 |
| permissions | -rw-r--r-- |
(* Title: HOLCF/sprod2.thy ID: $Id$ Author: Franz Regensburger Copyright 1993 Technische Universitaet Muenchen Class Instance **::(pcpo,pcpo)po *) Sprod2 = Sprod1 + arities "**" :: (pcpo,pcpo)po (* Witness for the above arity axiom is sprod1.ML *) rules (* instance of << for type ['a ** 'b] *) inst_sprod_po "(op <<)::['a ** 'b,'a ** 'b]=>bool = less_sprod" end