# HG changeset patch
# User mueller
# Date 910711624 -3600
# Node ID 136a51f95c91c645e393e431c44227ca96dbd58f
# Parent 1a708aa63ff0abc7f68cda6ad521fdaee44ba9d4
changed to a link;
diff -r 1a708aa63ff0 -r 136a51f95c91 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üller
Copyright 1997 Technische Universität München
-The distribution contains:
-
- - 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:
- Olaf Müller and Tobias Nipkow,
- Traces of I/O Automata in Isabelle/HOLCF.
-In TAPSOFT'97, Proc. of the 7th International Joint Conference on Theory and Practice of Software Development , LNCS 1224, 1997.
-
-
- 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:
-Olaf Müller and Tobias Nipkow,
-Combining Model Checking and Deduction for I/O Automata .
-In TACAS'95, Proc. of the 1st International Workshop on Tools and Algorithms for the Construction and Analysis of Systems , LNCS 1019, 1995.
-
- A proof of a Network Transmission Protocol (NTP subdirectory) using the theory of IOA described above. For details see:
-
- Tobias Nipkow, Konrad Slind.
-
-I/O Automata in Isabelle/HOL. In Types for Proofs and Programs,
-LNCS 996, 1995, 101-119.
-
-
+The distribution contains simulation relations, temporal logic, and an abstraction theory.
+Everything is based upon a domain-theoretic model of finite and infinite sequences.
+
+For details see IOA project.