author | paulson |
Wed, 05 Aug 1998 10:56:58 +0200 | |
changeset 5252 | 1b0f14d11142 |
child 5259 | 86d80749453f |
permissions | -rw-r--r-- |
(* Title: HOL/UNITY/Union.thy ID: $Id$ Author: Lawrence C Paulson, Cambridge University Computer Laboratory Copyright 1998 University of Cambridge Unions of programs From Misra's Chapter 5: Asynchronous Compositions of Programs *) Union = SubstAx + FP + constdefs Join :: "['a program, 'a program] => 'a program" "Join prgF prgG == (|Init = Init prgF Int Init prgG, Acts = Acts prgF Un Acts prgG|)" end