--- a/etc/settings Sat Nov 13 17:30:03 2004 +0100
+++ b/etc/settings Sun Nov 14 01:40:27 2004 +0100
@@ -224,8 +224,8 @@
# Einhoven model checker
#EINDHOVEN_HOME=/usr/local/bin
-# ZChaff, Version 2003.12.04 (SAT Solver)
-#ZCHAFF_HOME=/usr/local/bin
+# ZChaff, Version 2004.05.13 (SAT Solver)
+ZCHAFF_HOME=/home/webertj/bin
# BerkMin561 (SAT Solver)
#BERKMIN_HOME=/usr/local/bin
--- a/src/CTT/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/CTT/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,4 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<HTML><HEAD><TITLE>CTT/README</TITLE></HEAD><BODY>
@@ -11,8 +12,8 @@
Useful references on Constructive Type Theory:
<UL>
-<LI> B. Nordström, K. Petersson and J. M. Smith,<BR>
- Programming in Martin-Löf's Type Theory<BR>
+<LI> B. Nordstrm, K. Petersson and J. M. Smith,<BR>
+ Programming in Martin-Lf's Type Theory<BR>
(Oxford University Press, 1990)
<LI> Simon Thompson,<BR>
--- a/src/Cube/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/Cube/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,4 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
<HTML><HEAD><TITLE>Cube/README</TITLE></HEAD><BODY>
--- a/src/FOL/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/FOL/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<html><head><title>FOL/README</title></head><body>
<h2>FOL: First-Order Logic with Natural Deduction</h2>
--- a/src/HOL/Algebra/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/Algebra/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/Algebra/README.html</TITLE></HEAD><BODY>
@@ -12,7 +14,7 @@
<H2>GroupTheory, including Sylow's Theorem</H2>
-<P>These proofs are mainly by Florian Kammüller. (Later, Larry
+<P>These proofs are mainly by Florian Kammller. (Later, Larry
Paulson simplified some of the proofs.) These theories were indeed
the original motivation for locales.
--- a/src/HOL/Auth/Guard/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/Auth/Guard/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/Auth/Guard/README.html</TITLE></HEAD><BODY>
--- a/src/HOL/Auth/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/Auth/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY>
<H1>Auth--The Inductive Approach to Verifying Security Protocols</H1>
--- a/src/HOL/AxClasses/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/AxClasses/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<!-- $Id$ -->
<html>
--- a/src/HOL/Complex/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/Complex/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<HTML><HEAD><TITLE>HOL/Complex/README</TITLE>
<meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
</HEAD><BODY>
--- a/src/HOL/Hoare/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/Hoare/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<HTML><HEAD><TITLE>HOL/Hoare/ReadMe</TITLE></HEAD><BODY>
<H2>Hoare Logic for a Simple WHILE Language</H2>
--- a/src/HOL/IMPP/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/IMPP/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<!-- $Id$ -->
<HTML><HEAD>
<TITLE>HOL/IMPP/README</TITLE>
--- a/src/HOL/IOA/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/IOA/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<HTML><HEAD><TITLE>HOLCF/IOA/README</TITLE></HEAD><BODY>
<H3>IOA: A basic formalization of I/O automata in HOL</H3>
--- a/src/HOL/Induct/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/Induct/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/Induct/README</TITLE></HEAD><BODY>
--- a/src/HOL/Isar_examples/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/Isar_examples/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<!-- $Id$ -->
<html>
--- a/src/HOL/Lambda/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/Lambda/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/Lambda</TITLE></HEAD>
<BODY>
--- a/src/HOL/Library/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/Library/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<html>
<!-- $Id$ -->
--- a/src/HOL/Modelcheck/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/Modelcheck/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<html>
<!-- $Id$ -->
--- a/src/HOL/Prolog/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/Prolog/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<!-- $Id$ -->
<HTML><HEAD>
<TITLE>HOL/Prolog/README</TITLE>
--- a/src/HOL/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<html>
<!-- $Id$ -->
--- a/src/HOL/Real/HahnBanach/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/Real/HahnBanach/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,8 +1,10 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<HTML><HEAD><TITLE>HOL/Real/HahnBanach/README</TITLE></HEAD><BODY>
-<H3> The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar).</H3>
+<H3>The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar)</H3>
-Author: Gertrud Bauer, Technische Universität München<P>
+Author: Gertrud Bauer, Technische Universität München<P>
This directory contains the proof of the Hahn-Banach theorem for real vectorspaces,
following H. Heuser, Funktionalanalysis, p. 228 -232.
--- a/src/HOL/TLA/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/TLA/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<HTML><HEAD><TITLE>HOL/TLA</TITLE></HEAD><BODY>
<H2>TLA: Lamport's Temporal Logic of Actions</H2>
@@ -56,4 +58,4 @@
<!-- hhmts start -->
Last modified: Mon Jan 25 14:06:43 MET 1999
<!-- hhmts end -->
-</BODY></HTML>
\ No newline at end of file
+</BODY></HTML>
--- a/src/HOL/Tools/refute.ML Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/Tools/refute.ML Sun Nov 14 01:40:27 2004 +0100
@@ -1141,11 +1141,11 @@
(* unit -> (interpretation * model * arguments) option *)
fun interpret_groundtype () =
let
- val size = (if T = Term.propT then 2 else (the o assoc) (typs, T)) (* the model MUST specify a size for ground types *)
- val next = (if size=2 then next_idx+1 else next_idx+size) (* optimization for types with size 2 *)
- val _ = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ()) (* check if 'maxvars' is large enough *)
+ val size = (if T = Term.propT then 2 else (the o assoc) (typs, T)) (* the model MUST specify a size for ground types *)
+ val next = (if size=1 then next_idx else if size=2 then next_idx+1 else next_idx+size) (* optimization for types with size 1 or 2 *)
+ val _ = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ()) (* check if 'maxvars' is large enough *)
(* prop_formula list *)
- val fms = (if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
+ val fms = (if size=1 then [True] else if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
else (map BoolVar (next_idx upto (next_idx+size-1))))
(* interpretation *)
val intr = Leaf fms
@@ -1155,7 +1155,7 @@
(* prop_formula list -> prop_formula *)
fun exactly_one_true xs = SAnd (PropLogic.exists xs, one_of_two_false xs)
(* prop_formula *)
- val wf = (if size=2 then True else exactly_one_true fms)
+ val wf = (if size=1 then True else if size=2 then True else exactly_one_true fms)
in
(* extend the model, increase 'next_idx', add well-formedness condition *)
Some (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)})
@@ -1327,7 +1327,7 @@
in
(* ------------------------------------------------------------------------- *)
(* Providing interpretations directly is more efficient than unfolding the *)
- (* logical constants. IN HOL however, logical constants can themselves be *)
+ (* logical constants. In HOL however, logical constants can themselves be *)
(* arguments. "All" and "Ex" are then translated just like any other *)
(* constant, with the relevant axiom being added by 'collect_axioms'. *)
(* ------------------------------------------------------------------------- *)
@@ -1509,10 +1509,10 @@
(* recursively compute the size of the datatype *)
val size = size_of_dtyp typs' descr typ_assoc constrs
val next_idx = #next_idx args
- val next = (if size=2 then next_idx+1 else next_idx+size) (* optimization for types with size 2 *)
+ val next = (if size=1 then next_idx else if size=2 then next_idx+1 else next_idx+size) (* optimization for types with size 1 or size 2 *)
val _ = (if next-1>(#maxvars args) andalso (#maxvars args)>0 then raise MAXVARS_EXCEEDED else ()) (* check if 'maxvars' is large enough *)
(* prop_formula list *)
- val fms = (if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
+ val fms = (if size=1 then [True] else if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
else (map BoolVar (next_idx upto (next_idx+size-1))))
(* interpretation *)
val intr = Leaf fms
@@ -1522,7 +1522,7 @@
(* prop_formula list -> prop_formula *)
fun exactly_one_true xs = SAnd (PropLogic.exists xs, one_of_two_false xs)
(* prop_formula *)
- val wf = (if size=2 then True else exactly_one_true fms)
+ val wf = (if size=1 then True else if size=2 then True else exactly_one_true fms)
in
(* extend the model, increase 'next_idx', add well-formedness condition *)
Some (intr, (typs, (t, intr)::terms), {maxvars = #maxvars args, next_idx = next, bounds = #bounds args, wellformed = SAnd (#wellformed args, wf)})
--- a/src/HOL/UNITY/Comp/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/UNITY/Comp/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
--- a/src/HOL/UNITY/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/UNITY/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
--- a/src/HOL/UNITY/Simple/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/UNITY/Simple/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
--- a/src/HOL/W0/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/W0/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<HTML><HEAD><TITLE>HOL/W0/README</TITLE></HEAD>
<BODY>
--- a/src/HOL/ex/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOL/ex/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<!-- $Id$ -->
<HTML><HEAD><TITLE>HOL/ex/README</TITLE></HEAD><BODY>
--- a/src/HOLCF/FOCUS/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOLCF/FOCUS/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<HTML><HEAD><TITLE>HOLCF/README</TITLE></HEAD><BODY>
<H3>FOCUS: a theory of stream-processing functions Isabelle/<A HREF="..">HOLCF</A></H3>
--- a/src/HOLCF/IMP/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOLCF/IMP/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,8 +1,10 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<HTML><HEAD><TITLE>HOLCF/IMP/README</TITLE></HEAD><BODY>
-<H2>IMP --- A <KBD>WHILE</KBD>-language and its Semantics</H2>
+<H2>IMP -- A <KBD>WHILE</KBD>-language and its Semantics</H2>
This is the HOLCF-based denotational semantics of a simple
-<tt>WHILE</tt>-language. For a full description see <A
-HREF="../../HOL/IMP/index.html"> HOL/IMP</A>.
+<tt>WHILE</tt>-language. For a full description see <A
+HREF="../../HOL/IMP/index.html">HOL/IMP</A>.
</BODY></HTML>
--- a/src/HOLCF/IOA/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOLCF/IOA/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<HTML><HEAD><TITLE>HOLCF/IOA/README</TITLE></HEAD><BODY>
<H3>IOA: A formalization of I/O automata in HOLCF</H3>
--- a/src/HOLCF/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/HOLCF/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<HTML><HEAD><TITLE>HOLCF/README</TITLE></HEAD><BODY>
<H3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</H3>
--- a/src/LCF/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/LCF/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<HTML><HEAD><TITLE>LCF/README</TITLE></HEAD><BODY>
<H2>LCF: Logic for Computable Functions</H2>
--- a/src/Sequents/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/Sequents/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<!-- $Id$ -->
<HTML><HEAD><TITLE>Sequents/README</TITLE></HEAD><BODY>
--- a/src/ZF/AC/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/ZF/AC/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<!-- $Id$ -->
<HTML><HEAD><TITLE>ZF/AC/README</TITLE></HEAD><BODY>
@@ -16,7 +18,9 @@
<P>
The report
-<A HREF="http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz">Mechanizing Set Theory</A>, by Paulson and Grabczewski, describes both this development and ZF's theories of cardinals.
+<A HREF="http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz">Mechanizing Set Theory</A>,
+by Paulson and Grabczewski, describes both this development and ZF's theories
+of cardinals.
</body>
</html>
--- a/src/ZF/Coind/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/ZF/Coind/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<!-- $Id$ -->
<HTML><HEAD><TITLE>ZF/Coind/README</TITLE></HEAD><BODY>
--- a/src/ZF/Constructible/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/ZF/Constructible/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,8 +1,10 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<HTML><HEAD><TITLE>ZF/Constructible/README</TITLE></HEAD><BODY>
<H1>Constructible--Relative Consistency of the Axiom of Choice</H1>
-<P>Gödel's proof of the relative consistency of the axiom of choice is
+<P>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
<A HREF="http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf">reflection
@@ -25,4 +27,4 @@
HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
<A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
</ADDRESS>
-</BODY></HTML>
\ No newline at end of file
+</BODY></HTML>
--- a/src/ZF/IMP/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/ZF/IMP/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,12 +1,13 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<!-- $Id$ -->
<HTML><HEAD><TITLE>ZF/IMP/README</TITLE></HEAD><BODY>
<H2>IMP -- A <KBD>while</KBD>-language and two semantics</H2>
-The formalization of the denotational and operational semantics of
-a simple while-language together with an equivalence proof between the two
-semantics. The whole development essentially formalizes/transcribes chapters
-2 and 5 of
+The formalization of the denotational and operational semantics of a simple
+while-language together with an equivalence proof between the two semantics.
+The whole development essentially formalizes/transcribes chapters 2 and 5 of
<P>
<PRE>
@book{Winskel,
@@ -16,9 +17,9 @@
year = 1993}.
</PRE>
<P>
-There is a
-<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/loetz-sand.dvi.gz">
-report</A> by Lötzbeyer and Sandner.
+There is a
+<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/loetz-sand.dvi.gz">report</A>
+by Lötzbeyer and Sandner.
<P>
A much extended version of this development is found in
<A HREF="../../HOL/IMP/index.html">HOL/IMP</A>.
--- a/src/ZF/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/ZF/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<HTML><HEAD><TITLE>ZF/README</TITLE></HEAD><BODY>
<H2>ZF: Zermelo-Fraenkel Set Theory</H2>
@@ -23,7 +25,7 @@
<DT>Resid
<DD>subdirectory containing a proof of the Church-Rosser Theorem. It is
-by Ole Rasmussen, following the Coq proof by Gérard Huet.<P>
+by Ole Rasmussen, following the Coq proof by G�ard Huet.<P>
<DT>ex
<DD>subdirectory containing various examples.
--- a/src/ZF/Resid/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/ZF/Resid/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<!-- $Id$ -->
<HTML><HEAD><TITLE>ZF/Resid/README</TITLE></HEAD><BODY>
--- a/src/ZF/ex/README.html Sat Nov 13 17:30:03 2004 +0100
+++ b/src/ZF/ex/README.html Sun Nov 14 01:40:27 2004 +0100
@@ -1,3 +1,5 @@
+<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
+
<!-- $Id$ -->
<HTML><HEAD><TITLE>ZF/ex/README</TITLE></HEAD><BODY>