--- a/src/HOLCF/IOA/meta_theory/Compositionality.thy Wed May 21 11:27:32 1997 +0200
+++ b/src/HOLCF/IOA/meta_theory/Compositionality.thy Wed May 21 15:08:52 1997 +0200
@@ -1,21 +1,9 @@
(* Title: HOLCF/IOA/meta_theory/Compositionality.thy
- ID:
+ ID: $Id$
Author: Olaf M"uller
Copyright 1997 TU Muenchen
Compositionality of I/O automata
*)
-Compositionality = CompoTraces +
-
-rules
-
-compotraces
-"[| compat_ioas A B; compat_ioas B A;
- is_asig(asig_of A); is_asig(asig_of B)|]
- ==> traces(A||B) =
- {tr. (Filter (%a.a:act A)`tr : traces A &
- Filter (%a.a:act B)`tr : traces B &
- Forall (%x. x:ext(A||B)) tr)}"
-
-end
\ No newline at end of file
+Compositionality = Automata + Traces + CompoTraces