src/HOLCF/Sprod1.thy

Further development of matrix theory

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

Partial ordering for the strict product.
*)

Sprod1 = Sprod0 +

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

defs
  less_sprod_def "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"

end