src/HOL/README.html
changeset 7290 f1a37c379317
parent 4622 85aae356570c
child 7291 8aa66ddc0bea
     1.1 --- a/src/HOL/README.html	Thu Aug 19 16:33:53 1999 +0200
     1.2 +++ b/src/HOL/README.html	Thu Aug 19 16:54:38 1999 +0200
     1.3 @@ -20,8 +20,9 @@
     1.4  <DT>Induct
     1.5  <DD>examples of (co)inductive definitions
     1.6  
     1.7 -<DT>Integ
     1.8 -<DD>a theory of the integers including efficient integer calculations
     1.9 +<DT>Integ 
    1.10 +<DD>a development of the integers including efficient integer
    1.11 +calculations (part of the standard HOL environment)
    1.12  
    1.13  <DT>IOA
    1.14  <DD>extended example of Input/Output Automata
    1.15 @@ -29,8 +30,19 @@
    1.16  <DT>Lambda
    1.17  <DD>a proof of the Church-Rosser theorem for lambda-calculus
    1.18  
    1.19 +<DT>Real 
    1.20 +<DD>a development of the reals and hyper-reals, which are used in
    1.21 +non-standard analysis.  Also includes the positive rationals.  Used to build
    1.22 +the image HOL-Real.
    1.23 +
    1.24  <DT>Subst
    1.25 -<DD>subdirectory defining a theory of substitution and unification.
    1.26 +<DD>defines a theory of substitution and unification.
    1.27 +
    1.28 +<DT>Tools
    1.29 +<DD>holds code used to provide support for records, datatypes, induction, etc.
    1.30 +
    1.31 +<DT>UNITY
    1.32 +<DD>Chandy and Misra's UNITY formalism.
    1.33  </DL>
    1.34  
    1.35  Useful references on Higher-Order Logic: