author | paulson |
Tue, 31 Aug 1999 15:56:56 +0200 | |
changeset 7399 | cf780c2bcccf |
parent 7364 | a979e8a2ee18 |
child 8055 | bb15396278fb |
permissions | -rw-r--r-- |
(* Title: HOL/UNITY/Comp.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge Composition From Chandy and Sanders, "Reasoning About Program Composition" *) Comp = Union + instance program :: (term)ord defs component_def "F <= H == EX G. F Join G = H" strict_component_def "(F < (H::'a program)) == (F <= H & F ~= H)" end