src/HOLCF/Cprod1.thy

Further development of matrix theory

(*  Title:      HOLCF/Cprod1.thy
    ID:         $Id$
    Author:     Franz Regensburger
    License:    GPL (GNU GENERAL PUBLIC LICENSE)

Partial ordering for cartesian product of HOL theory prod.thy
*)

Cprod1 = Cfun3 +

default cpo

instance "*"::(sq_ord,sq_ord)sq_ord 

defs

  less_cprod_def "p1 << p2 == (fst p1<<fst p2 & snd p1 << snd p2)"

end