src/HOL/UNITY/Union.thy

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/UNITY/Union.thy	Wed Aug 05 10:56:58 1998 +0200
@@ -0,0 +1,19 @@
+(*  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