src/HOL/UNITY/Comp.thy
author paulson
Tue Aug 31 15:56:56 1999 +0200 (1999-08-31)
changeset 7399 cf780c2bcccf
parent 7364 a979e8a2ee18
child 8055 bb15396278fb
permissions -rw-r--r--
changed "component" infix in HOL/UNITY/Comp.thy to be overloaded <
     1 (*  Title:      HOL/UNITY/Comp.thy
     2     ID:         $Id$
     3     Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     4     Copyright   1998  University of Cambridge
     5 
     6 Composition
     7 
     8 From Chandy and Sanders, "Reasoning About Program Composition"
     9 *)
    10 
    11 Comp = Union +
    12 
    13 instance
    14   program :: (term)ord
    15 
    16 defs
    17 
    18   component_def   "F <= H == EX G. F Join G = H"
    19 
    20   strict_component_def   "(F < (H::'a program)) == (F <= H & F ~= H)"
    21 
    22 end