src/HOLCF/Sprod1.thy

converted to new-style theory

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

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