changeset 3807 82a99b090d9d
child 3849 3ea10bfd329d
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/TLA/README.html	Wed Oct 08 11:50:33 1997 +0200
@@ -0,0 +1,45 @@
+<H3>TLA: A formalization of TLA in HOL</H3>
+Author:     Stephan Merz<BR>
+Copyright   1997 Universit&auml;t M&uuml;nchen<P>
+The distribution contains a representation of Lamport's
+<A HREF="">
+Temporal Logic of Actions</A>
+in Isabelle/HOL.
+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.
+The distribution includes the following examples:
+  <li> a verification of Lamport's <quote>increment</quote> example
+  (subdirectory inc),<P>
+  <li> a proof that two buffers in a row implement a single buffer
+  (subdirectory buffer), and<P>
+   <li> the verification of Broy and Lamport's RPC-Memory example. For details see:<BR>
+        Mart&iacute;n Abadi, Leslie Lamport, and Stephan Merz: 
+        <A HREF="">
+        A TLA Solution to the RPC-Memory Specification Problem</A>.
+        In: <i>Formal System Specification</i>, LNCS 1169, 1996, 21-69.
+If you use Isabelle/TLA and have any comments, suggestions or contributions,
+please contact <A HREF="">Stephan Merz</A>.