| author | wenzelm |
| Thu Aug 27 20:46:36 1998 +0200 (1998-08-27) | |
| changeset 5400 | 645f46a24c72 |
| parent 243 | c22b85994e17 |
| permissions | -rw-r--r-- |
1 (* Title: HOLCF/ssum2.thy
2 ID: $Id$
3 Author: Franz Regensburger
4 Copyright 1993 Technische Universitaet Muenchen
6 Class Instance ++::(pcpo,pcpo)po
7 *)
9 Ssum2 = Ssum1 +
11 arities "++" :: (pcpo,pcpo)po
12 (* Witness for the above arity axiom is ssum1.ML *)
14 rules
16 (* instance of << for type ['a ++ 'b] *)
18 inst_ssum_po "(op <<)::['a ++ 'b,'a ++ 'b]=>bool = less_ssum"
20 end