Absolute URL's for documentation
authormerz
Mon Oct 13 11:00:06 1997 +0200 (1997-10-13)
changeset 38493ea10bfd329d
parent 3848 97bb3ff3c771
child 3850 305e5adfd7c8
Absolute URL's for documentation
src/HOL/TLA/README.html
     1.1 --- a/src/HOL/TLA/README.html	Mon Oct 13 10:31:21 1997 +0200
     1.2 +++ b/src/HOL/TLA/README.html	Mon Oct 13 11:00:06 1997 +0200
     1.3 @@ -13,13 +13,14 @@
     1.4  <p>
     1.5  
     1.6  The encoding is mainly oriented towards practical verification
     1.7 -examples. It does not contain a formalization of TLA's semantics;
     1.8 -instead, it is based on a 
     1.9 -<A HREF="doc/PTLA.dvi">complete axiomatization</A> of the "raw"
    1.10 -(stuttering-sensitive) variant of propositional TLA. It is
    1.11 -accompanied by a
    1.12 -<A HREF="doc/design.dvi">design note</A> that explains the basic 
    1.13 -setup and use of the prover.
    1.14 +examples. It does not contain a formalization of TLA's semantics,
    1.15 +although it could be an interesting exercise to add such a formalization
    1.16 +to the existing representation. Instead, it is based on a 
    1.17 +<A HREF="http://www4.informatik.tu-muenchen.de/~merz/papers/ptla.ps">complete axiomatization</A>
    1.18 +of the "raw" (stuttering-sensitive) variant of propositional TLA. 
    1.19 +There is also a
    1.20 +<A HREF="http://www4.informatik.tu-muenchen.de/~merz/papers/IsaTLADesign.ps">design note</A> 
    1.21 +that explains the basic setup and use of the prover.
    1.22  
    1.23  <p>
    1.24