src/HOLCF/Sprod1.thy
author paulson
Mon Dec 07 18:26:25 1998 +0100 (1998-12-07)
changeset 6019 0e55c2fb2ebb
parent 3323 194ae2e0c193
child 12030 46d57d0290a2
permissions -rw-r--r--
tidying
     1 (*  Title:      HOLCF/sprod1.thy
     2     ID:         $Id$
     3     Author:     Franz Regensburger
     4     Copyright   1993  Technische Universitaet Muenchen
     5 
     6 Partial ordering for the strict product
     7 *)
     8 
     9 Sprod1 = Sprod0 +
    10 
    11 instance "**"::(sq_ord,sq_ord)sq_ord 
    12 
    13 defs
    14   less_sprod_def "p1 << p2 == Isfst p1 << Isfst p2 & Issnd p1 << Issnd p2"
    15 
    16 end