isabelle: src/HOL/UNITY/Union.thy@82a5ca6290aa (annotated)

5252 1b0f14d11142 Union primitives and examples paulson parents: diff changeset	1	(* Title: HOL/UNITY/Union.thy
1b0f14d11142 Union primitives and examples paulson parents: diff changeset	2	ID: $Id$
1b0f14d11142 Union primitives and examples paulson parents: diff changeset	3	Author: Lawrence C Paulson, Cambridge University Computer Laboratory
1b0f14d11142 Union primitives and examples paulson parents: diff changeset	4	Copyright 1998 University of Cambridge
1b0f14d11142 Union primitives and examples paulson parents: diff changeset	5
1b0f14d11142 Union primitives and examples paulson parents: diff changeset	6	Unions of programs
1b0f14d11142 Union primitives and examples paulson parents: diff changeset	7
1b0f14d11142 Union primitives and examples paulson parents: diff changeset	8	From Misra's Chapter 5: Asynchronous Compositions of Programs
1b0f14d11142 Union primitives and examples paulson parents: diff changeset	9	*)
1b0f14d11142 Union primitives and examples paulson parents: diff changeset	10
1b0f14d11142 Union primitives and examples paulson parents: diff changeset	11	Union = SubstAx + FP +
1b0f14d11142 Union primitives and examples paulson parents: diff changeset	12
1b0f14d11142 Union primitives and examples paulson parents: diff changeset	13	constdefs
1b0f14d11142 Union primitives and examples paulson parents: diff changeset	14
1b0f14d11142 Union primitives and examples paulson parents: diff changeset	15	Join :: "['a program, 'a program] => 'a program"
1b0f14d11142 Union primitives and examples paulson parents: diff changeset	16	"Join prgF prgG == (\|Init = Init prgF Int Init prgG,
1b0f14d11142 Union primitives and examples paulson parents: diff changeset	17	Acts = Acts prgF Un Acts prgG\|)"
1b0f14d11142 Union primitives and examples paulson parents: diff changeset	18
1b0f14d11142 Union primitives and examples paulson parents: diff changeset	19	end

author	paulson
	Wed, 05 Aug 1998 10:57:25 +0200
changeset 5253	82a5ca6290aa
parent 5252	1b0f14d11142
child 5259	86d80749453f
permissions	-rw-r--r--