# HG changeset patch
# User paulson
# Date 935074478 -7200
# Node ID f1a37c379317c3348c3730057c29aa488b91e74d
# Parent 3b1b301467cdad89a2745552736fa5a58128f365
updated
diff -r 3b1b301467cd -r f1a37c379317 src/HOL/README.html
--- a/src/HOL/README.html Thu Aug 19 16:33:53 1999 +0200
+++ b/src/HOL/README.html Thu Aug 19 16:54:38 1999 +0200
@@ -20,8 +20,9 @@
Induct
examples of (co)inductive definitions
-Integ
-a theory of the integers including efficient integer calculations
+Integ
+a development of the integers including efficient integer
+calculations (part of the standard HOL environment)
IOA
extended example of Input/Output Automata
@@ -29,8 +30,19 @@
Lambda
a proof of the Church-Rosser theorem for lambda-calculus
+Real
+a development of the reals and hyper-reals, which are used in
+non-standard analysis. Also includes the positive rationals. Used to build
+the image HOL-Real.
+
Subst
-subdirectory defining a theory of substitution and unification.
+defines a theory of substitution and unification.
+
+Tools
+holds code used to provide support for records, datatypes, induction, etc.
+
+UNITY
+Chandy and Misra's UNITY formalism.
Useful references on Higher-Order Logic: