src/HOLCF/IOA/meta_theory/IOA.thy
author wenzelm
Thu, 22 Nov 2007 14:51:34 +0100
changeset 25456 6f79698f294d
parent 17233 41eee2e7b465
child 35174 e15040ae75d7
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     1
(*  Title:      HOLCF/IOA/meta_theory/IOA.thy
3275
3f53f2c876f4 changes for release 94-8
mueller
parents: 3071
diff changeset
     2
    ID:         $Id$
12218
wenzelm
parents: 4816
diff changeset
     3
    Author:     Olaf Müller
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     4
*)
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     5
17233
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     6
header {* The theory of I/O automata in HOLCF *}
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     7
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     8
theory IOA
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
     9
imports SimCorrectness Compositionality Deadlock
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    10
begin
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    11
41eee2e7b465 converted specifications to Isar theories;
wenzelm
parents: 14981
diff changeset
    12
end