src/HOLCF/Cprod1.thy
author kleing
Mon Jun 21 10:25:57 2004 +0200 (2004-06-21)
changeset 14981 e73f8140af78
parent 12030 46d57d0290a2
permissions -rw-r--r--
Merged in license change from Isabelle2004
     1 (*  Title:      HOLCF/Cprod1.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4 
     5 Partial ordering for cartesian product of HOL theory prod.thy
     6 *)
     7 
     8 Cprod1 = Cfun3 +
     9 
    10 default cpo
    11 
    12 instance "*"::(sq_ord,sq_ord)sq_ord 
    13 
    14 defs
    15 
    16   less_cprod_def "p1 << p2 == (fst p1<<fst p2 & snd p1 << snd p2)"
    17 
    18 end