src/HOLCF/Sprod1.thy

added split_eta_SetCompr2 (also to simpset), generalized SetCompr_Sigma_eq

(*  Title:      HOLCF/sprod1.thy
    ID:         $Id$
    Author:     Franz Regensburger
    Copyright   1993  Technische Universitaet Muenchen

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