--- a/src/HOLCF/IOA/README.html Mon Nov 09 15:50:56 1998 +0100
+++ b/src/HOLCF/IOA/README.html Tue Nov 10 16:27:04 1998 +0100
@@ -5,30 +5,11 @@
Author: Olaf Müller<BR>
Copyright 1997 Technische Universität München<P>
-The distribution contains:
-<UL>
- <li> A semantic model of the meta theory of I/O automata including proofs for the refinement notion
- and the compositionality of the model. For details see: <BR>
- Olaf Müller and Tobias Nipkow,
- <A HREF="http://www4.informatik.tu-muenchen.de/papers/tapsoft_mueller_1997_Conference.html">Traces of I/O Automata in Isabelle/HOLCF</A>.
-In <i> TAPSOFT'97, Proc. of the 7th International Joint Conference on Theory and Practice of Software Development </i>, LNCS 1224, 1997.<P>
-
- <li> A proof of the Alternating Bit Protocol (ABP subdirectory) with unbounded buffers using
- a combination of Isabelle and a model checker. This case study is performed within the
- theory of IOA described above. For details see:<BR>
-Olaf Müller and Tobias Nipkow,
-<A HREF="http://www4.informatik.tu-muenchen.de/papers/MuellerNipkow_TaAf1995.html">Combining Model Checking and Deduction for I/O Automata </A>.
-In <i> TACAS'95, Proc. of the 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems </i>, LNCS 1019, 1995.<P>
- <li> A proof of a Network Transmission Protocol (NTP subdirectory) using the theory of IOA described above. For details see:<BR>
-
- Tobias Nipkow, Konrad Slind.
-<A HREF=http://www4.informatik.tu-muenchen.de/~nipkow/pubs/types94.html>
-I/O Automata in Isabelle/HOL</A>. In <i>Types for Proofs and Programs</i>,
-LNCS 996, 1995, 101-119.
-
-</UL>
+The distribution contains simulation relations, temporal logic, and an abstraction theory.
+Everything is based upon a domain-theoretic model of finite and infinite sequences.
+<p>
+For details see <A HREF="http://www4.informatik.tu-muenchen.de/~isabelle/IOA/">IOA project</a>.
</BODY></HTML>
-