author | oheimb |
Fri, 29 Nov 1996 12:22:22 +0100 | |
changeset 2278 | d63ffafce255 |
parent 1479 | 21eb5e156d91 |
child 2640 | ee4dfce170a0 |
permissions | -rw-r--r-- |
(* Title: HOLCF/ssum2.thy ID: $Id$ Author: Franz Regensburger Copyright 1993 Technische Universitaet Muenchen Class Instance ++::(pcpo,pcpo)po *) Ssum2 = Ssum1 + arities "++" :: (pcpo,pcpo)po (* Witness for the above arity axiom is ssum1.ML *) rules (* instance of << for type ['a ++ 'b] *) inst_ssum_po "((op <<)::['a ++ 'b,'a ++ 'b]=>bool) = less_ssum" end