src/HOL/UNITY/Union.thy
changeset 5252 1b0f14d11142
child 5259 86d80749453f
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/UNITY/Union.thy	Wed Aug 05 10:56:58 1998 +0200
     1.3 @@ -0,0 +1,19 @@
     1.4 +(*  Title:      HOL/UNITY/Union.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     1.7 +    Copyright   1998  University of Cambridge
     1.8 +
     1.9 +Unions of programs
    1.10 +
    1.11 +From Misra's Chapter 5: Asynchronous Compositions of Programs
    1.12 +*)
    1.13 +
    1.14 +Union = SubstAx + FP +
    1.15 +
    1.16 +constdefs
    1.17 +
    1.18 +   Join :: "['a program, 'a program] => 'a program"
    1.19 +    "Join prgF prgG == (|Init = Init prgF Int Init prgG,
    1.20 +			 Acts = Acts prgF Un Acts prgG|)"
    1.21 +
    1.22 +end