# HG changeset patch
# User wenzelm
# Date 970841643 -7200
# Node ID d1972b445ecef623edf580660e2c0b19676b2c5d
# Parent 947b7b8b0a69b78becfd3962a13dd80efc098393
updated, improved;
diff -r 947b7b8b0a69 -r d1972b445ece src/HOL/README.html
--- a/src/HOL/README.html Fri Oct 06 16:11:53 2000 +0200
+++ b/src/HOL/README.html Fri Oct 06 16:14:03 2000 +0200
@@ -1,117 +1,129 @@
+
+
-HOL/README
-HOL: Higher-Order Logic
+HOL/README
-This directory contains the ML sources of the Isabelle system for
-Higher-Order Logic.
+
+
+HOL: Higher-Order Logic
-There are several subdirectories with examples:
-
-- ex
-
- general examples
+This directory contains the sources of the Isabelle system for
+Higher-Order Logic.
+
+
-
- Auth
-
- a new approach to verifying authentication protocols
+There are also several example sessions:
+
-- AxClasses
-
- a few axiomatic type class examples:
-
+- Algebra
+
- rings and univariate polynomials
+
+
- Auth
+
- a new approach to verifying authentication protocols
-
- Tutorial
- Some simple axclass demos that go along with the
-axclass Isabelle document (isatool doc axclass).
+
- AxClasses
+
- a few basic examples of using axiomatic type classes
+
+
- BCV
+
- generic model of bytecode verification, i.e. data-flow analysis
+for assembly languages with subtypes
-
- Group
-
- Some bits of group theory.
+
- HOL-Real
+
- a development of the reals and hyper-reals, which are used in
+non-standard analysis (builds the image HOL-Real)
-
- Lattice
-
- Basic theory of lattices and orders.
-
-
+ - HOL-Real-HahnBanach
+
- the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
-
- BCV
-
- generic model of bytecode verification, i.e. data-flow analysis
-for assembly languages with subtypes.
+
- HOL-Real-ex
+
- miscellaneous real number examples
+
+
- Hoare
+
- verification of imperative programs (verification conditions are
+generated automatically from pre/post conditions and loop invariants)
-
- Hoare
-
- verification of imperative programs; verification conditions are
-generated automatically from pre/post conditions and loop invariants.
+
- IMP
+
- mechanization of a large part of a semantics text by Glynn Winskel
-
- IMP
-
- mechanization of a large part of a semantics text by Glynn Winskel
+
- IMPP
+
- extension of IMP with local variables and mutually recursive
+procedures
-
- Induct
-
- examples of (co)inductive definitions
+
- IOA
+
- a simple theory of Input/Output Automata
+
+
- Induct
+
- examples of (co)inductive definitions
-
- Integ
-
- a development of the integers including efficient integer
-calculations (part of the standard HOL environment)
+
- Isar_examples
+
- several introductory examples using Isabelle/Isar
-
- IOA
-
- a simple theory of Input/Output Automata
+
- Lambda
+
- fundamental properties of lambda-calculus (Church-Rosser and termination)
-
- Isar_examples
-
- several introductory Isabelle/Isar examples
+
- Lattice
+
- lattices and order structures (in Isabelle/Isar)
-
- Lambda
-
- fundamental properties of lambda-calculus (Church-Rosser and termination)
+
- Lex
+
- verification of a simple lexical analyzer generator
-
- Lex
-
- verification of a simple lexical analyzer generator
+
- MicroJava
+
- 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.
-
- MiniML
-
- formalization of type inference for the language Mini-ML
+
- MiniML
+
- formalization of type inference for the language Mini-ML
-
- 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.
+
- Modelcheck
+
- basic setup for integration of some model checkers in Isabelle/HOL
-
- Real/HahnBanach
-
- the Hahn-Banach theorem for real vectorspaces (Isabelle/Isar).
+
- NumberTheory
+
- fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
+Fermat/Euler Theorem, Wilson's Theorem
-
- Subst
-
- defines a theory of substitution and unification.
+
- Prolog
+
- a (bare-bones) implementation of Lambda-Prolog
+
+
- Subst
+
- defines a theory of substitution and unification.
-
- TLA
-
- Lamport's Temporal Logic of Actions
+
- TLA
+
- Lamport's Temporal Logic of Actions (with separate example sessions)
-
- Tools
-
- holds code used to provide support for records, datatypes, induction, etc.
+
- UNITY
+
- Chandy and Misra's UNITY formalism
-
- UNITY
-
- Chandy and Misra's UNITY formalism.
+
- W0
+
- a precursor of MiniML, without let-expressions
-
- W0
-
- a precursor of MiniML, without let-expressions
-
+ - ex
+
- miscellaneous examples
+
+
Useful references on Higher-Order Logic:
-
-
-- P. B. Andrews,
- An Introduction to Mathematical Logic and Type Theory
- (Academic Press, 1986).
+
-
+
- P. B. Andrews,
+An Introduction to Mathematical Logic and Type Theory
+(Academic Press, 1986).
- - A. Church,
- A Formulation of the Simple Theory of Types
- (Journal of Symbolic Logic, 1940).
-
-
+
- A. Church,
+A Formulation of the Simple Theory of Types
+(Journal of Symbolic Logic, 1940).
- - M. J. C. Gordon and T. F. Melham (editors),
- Introduction to HOL: A theorem proving environment for higher order logic
- (Cambridge University Press, 1993).
-
-
+
- M. J. C. Gordon and T. F. Melham (editors),
+Introduction to HOL: A theorem proving environment for higher order logic
+(Cambridge University Press, 1993).
- - J. Lambek and P. J. Scott,
- Introduction to Higher Order Categorical Logic
- (Cambridge University Press, 1986).
+ - J. Lambek and P. J. Scott,
+Introduction to Higher Order Categorical Logic
+(Cambridge University Press, 1986).
-
+
-
+
+