# HG changeset patch
# User nipkow
# Date 1115052412 -7200
# Node ID 5df57194d064bed5916095e3069d4af5f5e34f6e
# Parent  5f0c8a3f022654caa0a3a148e6cb72c63f460bfd
*** empty log message ***

diff -r 5f0c8a3f0226 -r 5df57194d064 src/HOL/README.html
--- a/src/HOL/README.html	Mon May 02 18:29:29 2005 +0200
+++ b/src/HOL/README.html	Mon May 02 18:46:52 2005 +0200
@@ -29,24 +29,21 @@
 <dt>AxClasses
 <dd>a few basic examples of using axiomatic type classes
 
-<dt>BCV
-<dd>generic model of bytecode verification, i.e. data-flow analysis
-for assembly languages with subtypes
-
-<dt>HOL-Complex
+<dt>Complex
 <dd>a development of the complex numbers, the reals, and the hyper-reals,
 which are used in non-standard analysis (builds the image HOL-Complex)
 
-<dt>HOL-Complex-HahnBanach
-<dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
-
-<dt>HOL-Complex-ex
-<dd>miscellaneous real ans complex number examples
-
 <dt>Hoare
 <dd>verification of imperative programs (verification conditions are
 generated automatically from pre/post conditions and loop invariants)
 
+<dt>HoareParallel
+<dd>verification of shared-variable imperative programs a la Owicki-Gries.
+(verification conditions are generated automatically)
+
+<dt>Hyperreal
+<dd>Nonstandard analysis. Builds on Real and is part of Complex.
+
 <dt>IMP
 <dd>mechanization of a large part of a semantics text by Glynn Winskel
 
@@ -54,12 +51,15 @@
 <dd>extension of IMP with local variables and mutually recursive
 procedures
 
-<dt>IOA
-<dd>a simple theory of Input/Output Automata
+<dt>Import
+<dd>theories imported from other (HOL) theorem provers.
 
 <dt>Induct
 <dd>examples of (co)inductive definitions
 
+<dt>IOA
+<dd>a simple theory of Input/Output Automata
+
 <dt>Isar_examples
 <dd>several introductory examples using Isabelle/Isar
 
@@ -69,23 +69,41 @@
 <dt>Lattice
 <dd>lattices and order structures (in Isabelle/Isar)
 
+<dt>Library
+<dd>A collection of generic theories
+
+<dt>Matrix
+<dd>two-dimensional matrices
+
 <dt>MicroJava
 <dd>formalization of a fragment of Java, together with a corresponding
 virtual machine and a specification of its bytecode verifier and a
-lightweight bytecode verifier, including proofs of type-safety.
+lightweight bytecode verifier, including proofs of type-safety
 
 <dt>Modelcheck
 <dd>basic setup for integration of some model checkers in Isabelle/HOL
 
+<dt>NanoJava
+<dd>Haore Logic for a tiny fragment of Java
+
 <dt>NumberTheory
 <dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
-Fermat/Euler Theorem, Wilson's Theorem
+Fermat/Euler Theorem, Wilson's Theorem, Quadratic Reciprocity
 
 <dt>Prolog
 <dd>a (bare-bones) implementation of Lambda-Prolog
 
+<dt>Real
+<dd>the real numbers, part of Complex
+
+<dt>Real/HahnBanach
+<dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
+
+<dt>SET-Protocol
+<dd>verification of the SET Protocol
+
 <dt>Subst
-<dd>defines a theory of substitution and unification.
+<dd>a theory of substitution and unification.
 
 <dt>TLA
 <dd>Lamport's Temporal Logic of Actions (with separate example sessions)