summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | paulson |

Thu, 19 Aug 1999 16:54:38 +0200 | |

changeset 7290 | f1a37c379317 |

parent 7289 | 3b1b301467cd |

child 7291 | 8aa66ddc0bea |

updated

--- 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 @@ <DT>Induct <DD>examples of (co)inductive definitions -<DT>Integ -<DD>a theory of the integers including efficient integer calculations +<DT>Integ +<DD>a development of the integers including efficient integer +calculations (part of the standard HOL environment) <DT>IOA <DD>extended example of Input/Output Automata @@ -29,8 +30,19 @@ <DT>Lambda <DD>a proof of the Church-Rosser theorem for lambda-calculus +<DT>Real +<DD>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. + <DT>Subst -<DD>subdirectory defining a theory of substitution and unification. +<DD>defines a theory of substitution and unification. + +<DT>Tools +<DD>holds code used to provide support for records, datatypes, induction, etc. + +<DT>UNITY +<DD>Chandy and Misra's UNITY formalism. </DL> Useful references on Higher-Order Logic: