src/HOLCF/Ssum2.thy
author paulson
Wed, 15 Dec 2004 10:19:19 +0100
changeset 15412 7f373e478a5a
parent 14981 e73f8140af78
child 15568 41bfe19eabe2
permissions -rw-r--r--
*** empty log message ***

(*  Title:      HOLCF/ssum2.thy
    ID:         $Id$
    Author:     Franz Regensburger

Class Instance ++::(pcpo,pcpo)po
*)

Ssum2 = Ssum1 + 

instance "++"::(pcpo,pcpo)po (refl_less_ssum,antisym_less_ssum,trans_less_ssum)

end