Eliminated most occurrences of rule_format attribute.
(* 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