isabelle: src/HOL/HOLCF/IOA/meta_theory/IOA.thy@8f4a332500e4 (annotated)

42151 4da4fc77664b tuned headers; wenzelm parents: 40945 diff changeset	1	(* Title: HOL/HOLCF/IOA/meta_theory/IOA.thy
40945 b8703f63bfb2 recoded latin1 as utf8; wenzelm parents: 40774 diff changeset	2	Author: Olaf Müller
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	3	*)
3071 981258186b71 New meta theory for IOA based on HOLCF. mueller parents: diff changeset	4
17233 41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	5	header {* The theory of I/O automata in HOLCF *}
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	6
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	7	theory IOA
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	8	imports SimCorrectness Compositionality Deadlock
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	9	begin
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	10
41eee2e7b465 converted specifications to Isar theories; wenzelm parents: 14981 diff changeset	11	end