- Proofs are now hidden by default when generating documents
- New syntax for referring to theorems in lists
- Improvements to theory loader (relative and absolute paths)
(* 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