author | nipkow |
Sun, 22 Dec 2002 10:43:43 +0100 | |
changeset 13763 | f94b569cd610 |
parent 12030 | 46d57d0290a2 |
child 14981 | e73f8140af78 |
permissions | -rw-r--r-- |
(* Title: HOLCF/Cprod1.thy ID: $Id$ Author: Franz Regensburger License: GPL (GNU GENERAL PUBLIC LICENSE) Partial ordering for cartesian product of HOL theory prod.thy *) Cprod1 = Cfun3 + default cpo instance "*"::(sq_ord,sq_ord)sq_ord defs less_cprod_def "p1 << p2 == (fst p1<<fst p2 & snd p1 << snd p2)" end