--- a/src/HOL/TLA/README.html Mon Oct 13 10:31:21 1997 +0200
+++ b/src/HOL/TLA/README.html Mon Oct 13 11:00:06 1997 +0200
@@ -13,13 +13,14 @@
<p>
The encoding is mainly oriented towards practical verification
-examples. It does not contain a formalization of TLA's semantics;
-instead, it is based on a
-<A HREF="doc/PTLA.dvi">complete axiomatization</A> of the "raw"
-(stuttering-sensitive) variant of propositional TLA. It is
-accompanied by a
-<A HREF="doc/design.dvi">design note</A> that explains the basic
-setup and use of the prover.
+examples. It does not contain a formalization of TLA's semantics,
+although it could be an interesting exercise to add such a formalization
+to the existing representation. Instead, it is based on a
+<A HREF="http://www4.informatik.tu-muenchen.de/~merz/papers/ptla.ps">complete axiomatization</A>
+of the "raw" (stuttering-sensitive) variant of propositional TLA.
+There is also a
+<A HREF="http://www4.informatik.tu-muenchen.de/~merz/papers/IsaTLADesign.ps">design note</A>
+that explains the basic setup and use of the prover.
<p>