# HG changeset patch # User merz # Date 876733206 -7200 # Node ID 3ea10bfd329d26c5501b7c4d93e84439e9f3bbd0 # Parent 97bb3ff3c771d4becd5ee001590f99ccf9a56e1c Absolute URL's for documentation diff -r 97bb3ff3c771 -r 3ea10bfd329d src/HOL/TLA/README.html --- 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 @@
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 -complete axiomatization of the "raw" -(stuttering-sensitive) variant of propositional TLA. It is -accompanied by a -design note 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 +complete axiomatization +of the "raw" (stuttering-sensitive) variant of propositional TLA. +There is also a +design note +that explains the basic setup and use of the prover.