new entriues.
Thu, 19 Aug 1999 17:06:05 +0200
changeset 7291 8aa66ddc0bea
parent 7290 f1a37c379317
child 7292 dff3470c5c62
new entriues.
--- a/src/HOL/README.html	Thu Aug 19 16:54:38 1999 +0200
+++ b/src/HOL/README.html	Thu Aug 19 17:06:05 1999 +0200
@@ -14,6 +14,10 @@
 <DD>a new approach to verifying authentication protocols 
+<DD>verification of imperative programs; verification conditions are
+generated automatically from pre/post conditions and loop invariants.
 <DD>mechanization of a large part of a semantics text by Glynn Winskel
@@ -25,11 +29,17 @@
 calculations (part of the standard HOL environment)
-<DD>extended example of Input/Output Automata
+<DD>a simple theory of Input/Output Automata
 <DD>a proof of the Church-Rosser theorem for lambda-calculus
+<DD>verification of a simple lexical analyzer generator
+<DD>formalization of type inference for the language Mini-ML
 <DD>a development of the reals and hyper-reals, which are used in
 non-standard analysis.  Also includes the positive rationals.  Used to build
@@ -38,11 +48,17 @@
 <DD>defines a theory of substitution and unification.
+<DD>Lamport's Temporal Logic of Actions
 <DD>holds code used to provide support for records, datatypes, induction, etc.
 <DD>Chandy and Misra's UNITY formalism.
+<DD>a precursor of MiniML, without let-expressions
 Useful references on Higher-Order Logic: