Michael Dummett, Elements of Intuitionism (Oxford, 1977)
-
+
+
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/Algebra/README.html
--- a/src/HOL/Algebra/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Algebra/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
-HOL/Algebra/README.html
+
+
+
+
+
+ HOL/Algebra/README.html
+
+
+
Algebra --- Classical Algebra, using Explicit Structures and Locales
@@ -110,4 +118,5 @@
Clemens Ballarin.
-
+
+
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/Auth/Guard/README.html
--- a/src/HOL/Auth/Guard/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Auth/Guard/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
-HOL/Auth/Guard/README.html
+
+
+
+
+
+ HOL/Auth/Guard/README.html
+
+
+
Protocol-Independent Secrecy Results
@@ -58,4 +66,5 @@
Frederic Blanqui,
blanqui@lri.fr
-
+
+
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/Auth/README.html
--- a/src/HOL/Auth/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Auth/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,15 @@
-HOL/Auth/README
+
+
+
+
+
+
+ HOL/Auth/README
+
+
+
Auth--The Inductive Approach to Verifying Security Protocols
@@ -45,4 +54,5 @@
HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson,
lcp@cl.cam.ac.uk
-
+
+
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/AxClasses/README.html
--- a/src/HOL/AxClasses/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/AxClasses/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,10 +1,12 @@
+
-HOL/AxClasses
+
+ HOL/AxClasses
@@ -14,6 +16,5 @@
href="http://isabelle.in.tum.de/doc/axclass.pdf">Using Axiomatic Type
Classes in Isabelle. See also FOL/ex/NatClass for the natural
number example.
-
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/Complex/README.html
--- a/src/HOL/Complex/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Complex/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,8 +1,15 @@
-HOL/Complex/README
-
-
+
+
+
+
+
+
+ HOL/Complex/README
+
+
+
Complex: The Complex Numbers
This directory defines the type complex of the complex numbers,
@@ -56,5 +63,5 @@
Last modified $Date$
-
+
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/Hoare/README.html
--- a/src/HOL/Hoare/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Hoare/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,15 @@
-
HOL/Hoare/ReadMe
+
+
+
+
+
+
+ HOL/Hoare/ReadMe
+
+
+
Hoare Logic for a Simple WHILE Language
@@ -83,4 +92,5 @@
and the embeding is deep, i.e. there is a concrete datatype of programs. The
latter is not really necessary.
-
+
+
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/IMPP/README.html
--- a/src/HOL/IMPP/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/IMPP/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,9 +1,15 @@
-
-HOL/IMPP/README
-
+
+
+
+
+
+ HOL/IMPP/README
+
+
+
IMPP--An imperative language with procedures
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/IOA/README.html
--- a/src/HOL/IOA/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/IOA/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,18 +1,27 @@
-HOLCF/IOA/README
+
+
+
+
+
+
+ HOLCF/IOA/README
+
-IOA: A basic formalization of I/O automata in HOL
+
+
+IOA: A basic formalization of I/O automata in HOL
-Author: Konrad Slind, Tobias Nipkow and Olaf Müller
-Copyright 1995,1996 Technische Universität München
+Author: Konrad Slind, Tobias Nipkow and Olaf Müller
+Copyright 1995,1996 Technische Universität München
+
+
This directory contains a formalization of the meta theory of I/O automata in HOL.
-This formalization has been significantly changed and extended. The new version is available in the subdirectory HOLCF/IOA. There are also the proofs of two communication protocols which formerly
-have been here.
-
+This formalization has been significantly changed and extended. The new version
+is available in the subdirectory HOLCF/IOA. There are also the proofs of two
+communication protocols which formerly have been here.
-
-
-
-
+
+
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/Induct/README.html
--- a/src/HOL/Induct/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Induct/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
-
HOL/Induct/README
+
+
+
+
+
+ HOL/Induct/README
+
+
+
Induct--Examples of (Co)Inductive Definitions
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/Isar_examples/README.html
--- a/src/HOL/Isar_examples/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Isar_examples/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,10 +1,12 @@
+
-HOL/Isar_examples
+
+ HOL/Isar_examples
@@ -15,6 +17,5 @@
also the included document, or the Isabelle/Isar page for more
information.
-
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/Lambda/README.html
--- a/src/HOL/Lambda/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Lambda/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,14 @@
-HOL/Lambda
+
+
+
+
+
+ HOL/Lambda
+
+
Lambda Calculus in de Bruijn's Notation
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/Library/README.html
--- a/src/HOL/Library/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Library/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,10 +1,13 @@
+
+
-
-
-HOL-Library/README
+
+
+ HOL-Library/README
+
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/Modelcheck/README.html
--- a/src/HOL/Modelcheck/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Modelcheck/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,10 +1,13 @@
+
+
-
-
-HOL/Modelcheck
+
+
+ HOL/Modelcheck
+
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/Prolog/README.html
--- a/src/HOL/Prolog/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Prolog/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,15 +1,20 @@
-
-HOL/Prolog/README
-
+
+
+
+
+ HOL/Prolog/README
+
+
+
Prolog -- A bare-bones implementation of Lambda-Prolog
-This is a simple exploratory implementatin of
+This is a simple exploratory implementation of
Lambda-Prolog in HOL,
including some minimal examples (in Test.thy) and a more typical example
of a little functional language and its type system.
-
-
+
+
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/README.html
--- a/src/HOL/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,10 +1,13 @@
+
+
-
-
-HOL/README
+
+
+ HOL/README
+
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/Real/HahnBanach/README.html
--- a/src/HOL/Real/HahnBanach/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/Real/HahnBanach/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,15 @@
-HOL/Real/HahnBanach/README
+
+
+
+
+
+
+ HOL/Real/HahnBanach/README
+
+
+
The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar)
@@ -25,5 +34,5 @@
bauerg@in.tum.de
-
-
+
+
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/TLA/README.html
--- a/src/HOL/TLA/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/TLA/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,15 @@
-HOL/TLA
+
+
+
+
+
+
+ HOL/TLA
+
+
+
TLA: Lamport's Temporal Logic of Actions
@@ -56,6 +65,6 @@
Stephan Merz
-Last modified: Mon Jan 25 14:06:43 MET 1999
+Last modified: Sat Mar 5 00:54:49 CET 2005
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/UNITY/Comp/README.html
--- a/src/HOL/UNITY/Comp/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/UNITY/Comp/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
-HOL/UNITY/README
+
+
+
+
+
+ HOL/UNITY/README
+
+
+
UNITY: Examples Involving Program Composition
@@ -38,4 +46,5 @@
lcp@cl.cam.ac.uk
-
+
+
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/UNITY/README.html
--- a/src/HOL/UNITY/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/UNITY/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
-HOL/UNITY/README
+
+
+
+
+
+ HOL/UNITY/README
+
+
+
UNITY--Chandy and Misra's UNITY formalism
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/UNITY/Simple/README.html
--- a/src/HOL/UNITY/Simple/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/UNITY/Simple/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
-HOL/UNITY/README
+
+
+
+
+
+ HOL/UNITY/README
+
+
+
UNITY: Examples Involving Single Programs
@@ -35,4 +43,5 @@
lcp@cl.cam.ac.uk
-
+
+
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/W0/README.html
--- a/src/HOL/W0/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/W0/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,14 @@
-HOL/W0/README
+
+
+
+
+
+
+ HOL/W0/README
+
+
Type Inference for MiniML (without let)
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOL/ex/README.html
--- a/src/HOL/ex/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOL/ex/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
-HOL/ex/README
+
+
+
+
+
+ HOL/ex/README
+
+
+
ex--Miscellaneous Examples
@@ -41,4 +49,5 @@
lcp@cl.cam.ac.uk
-
+
+
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOLCF/FOCUS/README.html
--- a/src/HOLCF/FOCUS/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOLCF/FOCUS/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,13 @@
-HOLCF/README
+
+
+
+
+ HOLCF/README
+
+
+
FOCUS: a theory of stream-processing functions Isabelle/HOLCF
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOLCF/IMP/README.html
--- a/src/HOLCF/IMP/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOLCF/IMP/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,10 +1,20 @@
-HOLCF/IMP/README
+
+
+
+
+
+
+ HOLCF/IMP/README
+
+
+
IMP -- A WHILE-language and its Semantics
This is the HOLCF-based denotational semantics of a simple
WHILE-language. For a full description see HOL/IMP.
-
+
+
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOLCF/IOA/README.html
--- a/src/HOLCF/IOA/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOLCF/IOA/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,15 @@
-HOLCF/IOA/README
+
+
+
+
+
+
+ HOLCF/IOA/README
+
+
+
IOA: A formalization of I/O automata in HOLCF
diff -r f07e865d9d40 -r 7219facb3fd0 src/HOLCF/README.html
--- a/src/HOLCF/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/HOLCF/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,8 +1,17 @@
-HOLCF/README
+
+
+
-HOLCF: A higher-order version of LCF based on Isabelle/HOL
+
+
+ HOLCF/README
+
+
+
+
+HOLCF: A higher-order version of LCF based on Isabelle/HOL
HOLCF is the definitional extension of Church's Higher-Order Logic with
Scott's Logic for Computable Functions that has been implemented in the
@@ -10,25 +19,29 @@
about functional programs. HOLCF supports standard domain theory (in particular
fixpoint reasoning and recursive domain equations) but also coinductive
arguments about lazy datatypes.
-
+
+
+
The most recent description of HOLCF is found here:
-
-A detailed description (in german) of the entire development can be found in:
+
-
+A detailed description (in German) of the entire development can be found in:
+
+
A short survey is available in:
-
+
-
+
+
+
diff -r f07e865d9d40 -r 7219facb3fd0 src/LCF/README.html
--- a/src/LCF/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/LCF/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,15 @@
-LCF/README
+
+
+
+
+
+
+ LCF/README
+
+
+
LCF: Logic for Computable Functions
diff -r f07e865d9d40 -r 7219facb3fd0 src/Sequents/README.html
--- a/src/Sequents/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/Sequents/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
-Sequents/README
+
+
+
+
+
+ Sequents/README
+
+
+
Sequents: Various Sequent Calculi
diff -r f07e865d9d40 -r 7219facb3fd0 src/ZF/AC/README.html
--- a/src/ZF/AC/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/ZF/AC/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
-ZF/AC/README
+
+
+
+
+
+ ZF/AC/README
+
+
+
AC -- Equivalents of the Axiom of Choice
@@ -9,7 +17,7 @@
-@book{rubin&rubin,
+@book{rubin&rubin,
author = "Herman Rubin and Jean E. Rubin",
title = "Equivalents of the Axiom of Choice, {II}",
publisher = "North-Holland",
diff -r f07e865d9d40 -r 7219facb3fd0 src/ZF/Coind/README.html
--- a/src/ZF/Coind/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/ZF/Coind/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
-ZF/Coind/README
+
+
+
+
+
+ ZF/Coind/README
+
+
+
Coind -- A Coinduction Example
diff -r f07e865d9d40 -r 7219facb3fd0 src/ZF/Constructible/README.html
--- a/src/ZF/Constructible/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/ZF/Constructible/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,30 +1,41 @@
-ZF/Constructible/README
+
+
+
-Constructible--Relative Consistency of the Axiom of Choice
+
+
+ ZF/Constructible/README
+
-Gödel's proof of the relative consistency of the axiom of choice is
+
+Constructible--Relative Consistency of the Axiom of Choice
+
+Gödel's proof of the relative consistency of the axiom of choice is
mechanized using Isabelle/ZF. The proof builds upon a previous mechanization
of the
-reflection
-theorem. The heavy reliance on metatheory in the original proof makes the
+reflection
+theorem. The heavy reliance on metatheory in the original proof makes the
formalization unusually long, and not entirely satisfactory: two parts of the
proof do not fit together. It seems impossible to solve these problems
without formalizing the metatheory. However, the present development follows
-a standard textbook, Kunen's Set Theory, and could support the
+a standard textbook, Kunen's Set Theory, and could support the
formalization of further material from that book. It also serves as an
example of what to expect when deep mathematics is formalized.
A paper describing this development is
-available.
+available.
-
-Last modified $Date$
+
+
+
-
-Larry Paulson,
-lcp@cl.cam.ac.uk
-
-
+Last modified $Date$
+
+
+Larry Paulson,
+lcp@cl.cam.ac.uk
+
+
+
diff -r f07e865d9d40 -r 7219facb3fd0 src/ZF/IMP/README.html
--- a/src/ZF/IMP/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/ZF/IMP/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,7 +1,15 @@
-ZF/IMP/README
+
+
+
+
+
+ ZF/IMP/README
+
+
+
IMP -- A while-language and two semantics
diff -r f07e865d9d40 -r 7219facb3fd0 src/ZF/README.html
--- a/src/ZF/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/ZF/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,6 +1,15 @@
-ZF/README
+
+
+
+
+
+
+ ZF/README
+
+
+
ZF: Zermelo-Fraenkel Set Theory
diff -r f07e865d9d40 -r 7219facb3fd0 src/ZF/Resid/README.html
--- a/src/ZF/Resid/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/ZF/Resid/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,29 +1,36 @@
-ZF/Resid/README
+
+
-Resid -- A theory of residuals
+
+
+ ZF/Resid/README
+
+
+
+
+Resid -- A theory of residuals
Ole Rasmussen has ported to Isabelle/ZF the Coq proofs described in the
article
-
-
+
+
+
@Article{huet-residual,
- author = "{G\'erard} Huet",
- title = "Residual Theory in $\lambda$-Calculus: A Formal
- Development",
- journal = JFP,
- year = 1994,
- volume = 4,
- number = 3,
- pages = "371--394"}
-
+ author = "{G\'erard} Huet",
+ title = "Residual Theory in $\lambda$-Calculus: A Formal Development",
+ journal = JFP,
+ year = 1994,
+ volume = 4,
+ number = 3,
+ pages = "371--394"}
+
-See Rasmussen's report
-The Church-Rosser Theorem in Isabelle: A Proof Porting
- Experiment.
+See Rasmussen's report The Church-Rosser Theorem in Isabelle: A Proof Porting Experiment.
diff -r f07e865d9d40 -r 7219facb3fd0 src/ZF/ex/README.html
--- a/src/ZF/ex/README.html Mon Mar 07 18:40:36 2005 +0100
+++ b/src/ZF/ex/README.html Mon Mar 07 19:17:07 2005 +0100
@@ -1,16 +1,23 @@
-ZF/ex/README
+
+
-ZF general examples
+
+
+ ZF/ex/README
+
-Examples on this directory include a simple form of Ramsey's theorem. A
-report
-is available.
+
+
+ZF general examples
-Several (co)inductive and (co)datatype definitions are presented. One report describes the theoretical foundations of datatypes while another describes the package that automates their declaration.
+Examples on this directory include a simple form of Ramsey's theorem. A report is available.
+
+
+
+Several (co)inductive and (co)datatype definitions are presented. One report describes the theoretical foundations of datatypes while another describes the package that automates their declaration.