src/HOLCF/IOA/meta_theory/IOA.thy
author wenzelm
Wed, 29 Jun 2005 15:13:25 +0200
changeset 16595 e64fb2cf50cb
parent 14981 e73f8140af78
child 17233 41eee2e7b465
permissions -rw-r--r--
added implies_intr_hyps (from thm.ML);
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
3071
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     4
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     5
The theory of I/O automata in HOLCF.
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     6
*)   
981258186b71 New meta theory for IOA based on HOLCF.
mueller
parents:
diff changeset
     7
	       
4816
64f075872f69 simplification of explicit theory usage and merges
oheimb
parents: 4565
diff changeset
     8
IOA = SimCorrectness + Compositionality + Deadlock