src/HOL/README.html
changeset 15910 5df57194d064
parent 15582 7219facb3fd0
child 15916 1314ef1e49dd
     1.1 --- a/src/HOL/README.html	Mon May 02 18:29:29 2005 +0200
     1.2 +++ b/src/HOL/README.html	Mon May 02 18:46:52 2005 +0200
     1.3 @@ -29,24 +29,21 @@
     1.4  <dt>AxClasses
     1.5  <dd>a few basic examples of using axiomatic type classes
     1.6  
     1.7 -<dt>BCV
     1.8 -<dd>generic model of bytecode verification, i.e. data-flow analysis
     1.9 -for assembly languages with subtypes
    1.10 -
    1.11 -<dt>HOL-Complex
    1.12 +<dt>Complex
    1.13  <dd>a development of the complex numbers, the reals, and the hyper-reals,
    1.14  which are used in non-standard analysis (builds the image HOL-Complex)
    1.15  
    1.16 -<dt>HOL-Complex-HahnBanach
    1.17 -<dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
    1.18 -
    1.19 -<dt>HOL-Complex-ex
    1.20 -<dd>miscellaneous real ans complex number examples
    1.21 -
    1.22  <dt>Hoare
    1.23  <dd>verification of imperative programs (verification conditions are
    1.24  generated automatically from pre/post conditions and loop invariants)
    1.25  
    1.26 +<dt>HoareParallel
    1.27 +<dd>verification of shared-variable imperative programs a la Owicki-Gries.
    1.28 +(verification conditions are generated automatically)
    1.29 +
    1.30 +<dt>Hyperreal
    1.31 +<dd>Nonstandard analysis. Builds on Real and is part of Complex.
    1.32 +
    1.33  <dt>IMP
    1.34  <dd>mechanization of a large part of a semantics text by Glynn Winskel
    1.35  
    1.36 @@ -54,12 +51,15 @@
    1.37  <dd>extension of IMP with local variables and mutually recursive
    1.38  procedures
    1.39  
    1.40 -<dt>IOA
    1.41 -<dd>a simple theory of Input/Output Automata
    1.42 +<dt>Import
    1.43 +<dd>theories imported from other (HOL) theorem provers.
    1.44  
    1.45  <dt>Induct
    1.46  <dd>examples of (co)inductive definitions
    1.47  
    1.48 +<dt>IOA
    1.49 +<dd>a simple theory of Input/Output Automata
    1.50 +
    1.51  <dt>Isar_examples
    1.52  <dd>several introductory examples using Isabelle/Isar
    1.53  
    1.54 @@ -69,23 +69,41 @@
    1.55  <dt>Lattice
    1.56  <dd>lattices and order structures (in Isabelle/Isar)
    1.57  
    1.58 +<dt>Library
    1.59 +<dd>A collection of generic theories
    1.60 +
    1.61 +<dt>Matrix
    1.62 +<dd>two-dimensional matrices
    1.63 +
    1.64  <dt>MicroJava
    1.65  <dd>formalization of a fragment of Java, together with a corresponding
    1.66  virtual machine and a specification of its bytecode verifier and a
    1.67 -lightweight bytecode verifier, including proofs of type-safety.
    1.68 +lightweight bytecode verifier, including proofs of type-safety
    1.69  
    1.70  <dt>Modelcheck
    1.71  <dd>basic setup for integration of some model checkers in Isabelle/HOL
    1.72  
    1.73 +<dt>NanoJava
    1.74 +<dd>Haore Logic for a tiny fragment of Java
    1.75 +
    1.76  <dt>NumberTheory
    1.77  <dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
    1.78 -Fermat/Euler Theorem, Wilson's Theorem
    1.79 +Fermat/Euler Theorem, Wilson's Theorem, Quadratic Reciprocity
    1.80  
    1.81  <dt>Prolog
    1.82  <dd>a (bare-bones) implementation of Lambda-Prolog
    1.83  
    1.84 +<dt>Real
    1.85 +<dd>the real numbers, part of Complex
    1.86 +
    1.87 +<dt>Real/HahnBanach
    1.88 +<dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
    1.89 +
    1.90 +<dt>SET-Protocol
    1.91 +<dd>verification of the SET Protocol
    1.92 +
    1.93  <dt>Subst
    1.94 -<dd>defines a theory of substitution and unification.
    1.95 +<dd>a theory of substitution and unification.
    1.96  
    1.97  <dt>TLA
    1.98  <dd>Lamport's Temporal Logic of Actions (with separate example sessions)