changed to a link;
authormueller
Tue, 10 Nov 1998 16:27:04 +0100
changeset 5843 136a51f95c91
parent 5842 1a708aa63ff0
child 5844 2886310fb5e9
changed to a link;
src/HOLCF/IOA/README.html
--- 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&uuml;ller<BR>
 Copyright   1997 Technische Universit&auml;t M&uuml;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&uuml;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&uuml;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>
 
 
-