--- a/src/HOL/README.html Tue Mar 12 20:03:04 2013 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,121 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
-
-<html>
-
-<head>
- <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
- <title>HOL/README</title>
-</head>
-
-<body>
-
-<h2>HOL: Higher-Order Logic</h2>
-
-These are the main sources of the Isabelle system for Higher-Order Logic.
-
-<p>
-
-There are also several example sessions:
-<dl>
-
-<dt>Algebra
-<dd>rings and univariate polynomials
-
-<dt>Auth
-<dd>a new approach to verifying authentication protocols
-
-<dt>AxClasses
-<dd>a few basic examples of using axiomatic type classes
-
-<dt>Complex
-<dd>a development of the complex numbers, the reals, and the hyper-reals,
-which are used in non-standard analysis (builds the image HOL-Complex)
-
-<dt>Hoare
-<dd>verification of imperative programs (verification conditions are
-generated automatically from pre/post conditions and loop invariants)
-
-<dt>HoareParallel
-<dd>verification of shared-variable imperative programs a la Owicki-Gries.
-(verification conditions are generated automatically)
-
-<dt>Hyperreal
-<dd>Nonstandard analysis. Builds on Real and is part of Complex.
-
-<dt>IMP
-<dd>mechanization of a large part of a semantics text by Glynn Winskel
-
-<dt>IMPP
-<dd>extension of IMP with local variables and mutually recursive
-procedures
-
-<dt>Import
-<dd>theories imported from other (HOL) theorem provers.
-
-<dt>Induct
-<dd>examples of (co)inductive definitions
-
-<dt>IOA
-<dd>a simple theory of Input/Output Automata
-
-<dt>Isar_Examples
-<dd>several introductory examples using Isabelle/Isar
-
-<dt>Lambda
-<dd>fundamental properties of lambda-calculus (Church-Rosser and termination)
-
-<dt>Lattice
-<dd>lattices and order structures (in Isabelle/Isar)
-
-<dt>Library
-<dd>A collection of generic theories
-
-<dt>Matrix
-<dd>two-dimensional matrices
-
-<dt>MicroJava
-<dd>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
-
-<dt>Modelcheck
-<dd>basic setup for integration of some model checkers in Isabelle/HOL
-
-<dt>NanoJava
-<dd>Haore Logic for a tiny fragment of Java
-
-<dt>NumberTheory
-<dd>fundamental Theorem of Arithmetic, Chinese Remainder Theorem,
-Fermat/Euler Theorem, Wilson's Theorem, Quadratic Reciprocity
-
-<dt>Prolog
-<dd>a (bare-bones) implementation of Lambda-Prolog
-
-<dt>Real
-<dd>the real numbers, part of Complex
-
-<dt>Hahn_Banach
-<dd>the Hahn-Banach theorem for real vector spaces (in Isabelle/Isar)
-
-<dt>SET_Protocol
-<dd>verification of the SET Protocol
-
-<dt>Subst
-<dd>a theory of substitution and unification.
-
-<dt>TLA
-<dd>Lamport's Temporal Logic of Actions (with separate example sessions)
-
-<dt>UNITY
-<dd>Chandy and Misra's UNITY formalism
-
-<dt>W0
-<dd>a precursor of MiniML, without let-expressions
-
-<dt>ex
-<dd>miscellaneous examples
-
-</dl>
-
-</body>
-</html>