author | wenzelm |
Wed, 29 Apr 1998 11:34:11 +0200 | |
changeset 4859 | 53aa2bc0a22d |
parent 3323 | 194ae2e0c193 |
child 12030 | 46d57d0290a2 |
permissions | -rw-r--r-- |
(* Title: HOLCF/Cprod1.thy ID: $Id$ Author: Franz Regensburger Copyright 1993 Technische Universitaet Muenchen 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