DOCTYPE declaration added
authorwebertj
Sun Nov 14 01:40:27 2004 +0100 (2004-11-14)
changeset 15283f21466450330
parent 15282 765d5d6e4468
child 15284 f14c6c057172
DOCTYPE declaration added
etc/settings
src/CTT/README.html
src/Cube/README.html
src/FOL/README.html
src/HOL/Algebra/README.html
src/HOL/Auth/Guard/README.html
src/HOL/Auth/README.html
src/HOL/AxClasses/README.html
src/HOL/Complex/README.html
src/HOL/Hoare/README.html
src/HOL/IMPP/README.html
src/HOL/IOA/README.html
src/HOL/Induct/README.html
src/HOL/Isar_examples/README.html
src/HOL/Lambda/README.html
src/HOL/Library/README.html
src/HOL/Modelcheck/README.html
src/HOL/Prolog/README.html
src/HOL/README.html
src/HOL/Real/HahnBanach/README.html
src/HOL/TLA/README.html
src/HOL/Tools/refute.ML
src/HOL/UNITY/Comp/README.html
src/HOL/UNITY/README.html
src/HOL/UNITY/Simple/README.html
src/HOL/W0/README.html
src/HOL/ex/README.html
src/HOLCF/FOCUS/README.html
src/HOLCF/IMP/README.html
src/HOLCF/IOA/README.html
src/HOLCF/README.html
src/LCF/README.html
src/Sequents/README.html
src/ZF/AC/README.html
src/ZF/Coind/README.html
src/ZF/Constructible/README.html
src/ZF/IMP/README.html
src/ZF/README.html
src/ZF/Resid/README.html
src/ZF/ex/README.html
     1.1 --- a/etc/settings	Sat Nov 13 17:30:03 2004 +0100
     1.2 +++ b/etc/settings	Sun Nov 14 01:40:27 2004 +0100
     1.3 @@ -224,8 +224,8 @@
     1.4  # Einhoven model checker
     1.5  #EINDHOVEN_HOME=/usr/local/bin
     1.6  
     1.7 -# ZChaff, Version 2003.12.04 (SAT Solver)
     1.8 -#ZCHAFF_HOME=/usr/local/bin
     1.9 +# ZChaff, Version 2004.05.13 (SAT Solver)
    1.10 +ZCHAFF_HOME=/home/webertj/bin
    1.11  
    1.12  # BerkMin561 (SAT Solver)
    1.13  #BERKMIN_HOME=/usr/local/bin
     2.1 --- a/src/CTT/README.html	Sat Nov 13 17:30:03 2004 +0100
     2.2 +++ b/src/CTT/README.html	Sun Nov 14 01:40:27 2004 +0100
     2.3 @@ -1,3 +1,4 @@
     2.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     2.5  
     2.6  <HTML><HEAD><TITLE>CTT/README</TITLE></HEAD><BODY>
     2.7  
     2.8 @@ -11,8 +12,8 @@
     2.9  Useful references on Constructive Type Theory:
    2.10  
    2.11  <UL>
    2.12 -<LI>	B. Nordström, K. Petersson and J. M. Smith,<BR>
    2.13 -	Programming in Martin-Löf's Type Theory<BR>
    2.14 +<LI>	B. Nordstrm, K. Petersson and J. M. Smith,<BR>
    2.15 +	Programming in Martin-Lf's Type Theory<BR>
    2.16  	(Oxford University Press, 1990)
    2.17  
    2.18  <LI>	Simon Thompson,<BR>
     3.1 --- a/src/Cube/README.html	Sat Nov 13 17:30:03 2004 +0100
     3.2 +++ b/src/Cube/README.html	Sun Nov 14 01:40:27 2004 +0100
     3.3 @@ -1,3 +1,4 @@
     3.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     3.5  
     3.6  <HTML><HEAD><TITLE>Cube/README</TITLE></HEAD><BODY>
     3.7  
     4.1 --- a/src/FOL/README.html	Sat Nov 13 17:30:03 2004 +0100
     4.2 +++ b/src/FOL/README.html	Sun Nov 14 01:40:27 2004 +0100
     4.3 @@ -1,3 +1,5 @@
     4.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     4.5 +
     4.6  <html><head><title>FOL/README</title></head><body>
     4.7  
     4.8  <h2>FOL: First-Order Logic with Natural Deduction</h2>
     5.1 --- a/src/HOL/Algebra/README.html	Sat Nov 13 17:30:03 2004 +0100
     5.2 +++ b/src/HOL/Algebra/README.html	Sun Nov 14 01:40:27 2004 +0100
     5.3 @@ -1,3 +1,5 @@
     5.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     5.5 +
     5.6  <!-- $Id$ -->
     5.7  <HTML><HEAD><TITLE>HOL/Algebra/README.html</TITLE></HEAD><BODY>
     5.8  
     5.9 @@ -12,7 +14,7 @@
    5.10  
    5.11  <H2>GroupTheory, including Sylow's Theorem</H2>
    5.12  
    5.13 -<P>These proofs are mainly by Florian Kammüller.  (Later, Larry
    5.14 +<P>These proofs are mainly by Florian Kammller.  (Later, Larry
    5.15  Paulson simplified some of the proofs.)  These theories were indeed
    5.16  the original motivation for locales.
    5.17  
     6.1 --- a/src/HOL/Auth/Guard/README.html	Sat Nov 13 17:30:03 2004 +0100
     6.2 +++ b/src/HOL/Auth/Guard/README.html	Sun Nov 14 01:40:27 2004 +0100
     6.3 @@ -1,3 +1,5 @@
     6.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     6.5 +
     6.6  <!-- $Id$ -->
     6.7  <HTML><HEAD><TITLE>HOL/Auth/Guard/README.html</TITLE></HEAD><BODY>
     6.8  
     7.1 --- a/src/HOL/Auth/README.html	Sat Nov 13 17:30:03 2004 +0100
     7.2 +++ b/src/HOL/Auth/README.html	Sun Nov 14 01:40:27 2004 +0100
     7.3 @@ -1,3 +1,5 @@
     7.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     7.5 +
     7.6  <HTML><HEAD><TITLE>HOL/Auth/README</TITLE></HEAD><BODY>
     7.7  
     7.8  <H1>Auth--The Inductive Approach to Verifying Security Protocols</H1>
     8.1 --- a/src/HOL/AxClasses/README.html	Sat Nov 13 17:30:03 2004 +0100
     8.2 +++ b/src/HOL/AxClasses/README.html	Sun Nov 14 01:40:27 2004 +0100
     8.3 @@ -1,3 +1,5 @@
     8.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     8.5 +
     8.6  <!-- $Id$ -->
     8.7  <html>
     8.8  
     9.1 --- a/src/HOL/Complex/README.html	Sat Nov 13 17:30:03 2004 +0100
     9.2 +++ b/src/HOL/Complex/README.html	Sun Nov 14 01:40:27 2004 +0100
     9.3 @@ -1,3 +1,5 @@
     9.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
     9.5 +
     9.6  <HTML><HEAD><TITLE>HOL/Complex/README</TITLE>
     9.7  		<meta http-equiv="content-type" content="text/html;charset=iso-8859-1">
     9.8  	</HEAD><BODY>
    10.1 --- a/src/HOL/Hoare/README.html	Sat Nov 13 17:30:03 2004 +0100
    10.2 +++ b/src/HOL/Hoare/README.html	Sun Nov 14 01:40:27 2004 +0100
    10.3 @@ -1,3 +1,5 @@
    10.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    10.5 +
    10.6  <HTML><HEAD><TITLE>HOL/Hoare/ReadMe</TITLE></HEAD><BODY>
    10.7  
    10.8  <H2>Hoare Logic for a Simple WHILE Language</H2>
    11.1 --- a/src/HOL/IMPP/README.html	Sat Nov 13 17:30:03 2004 +0100
    11.2 +++ b/src/HOL/IMPP/README.html	Sun Nov 14 01:40:27 2004 +0100
    11.3 @@ -1,3 +1,5 @@
    11.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    11.5 +
    11.6  <!-- $Id$ -->
    11.7  <HTML><HEAD>
    11.8  <TITLE>HOL/IMPP/README</TITLE>
    12.1 --- a/src/HOL/IOA/README.html	Sat Nov 13 17:30:03 2004 +0100
    12.2 +++ b/src/HOL/IOA/README.html	Sun Nov 14 01:40:27 2004 +0100
    12.3 @@ -1,3 +1,5 @@
    12.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    12.5 +
    12.6  <HTML><HEAD><TITLE>HOLCF/IOA/README</TITLE></HEAD><BODY>
    12.7  
    12.8  <H3>IOA: A basic formalization of I/O automata in HOL</H3>
    13.1 --- a/src/HOL/Induct/README.html	Sat Nov 13 17:30:03 2004 +0100
    13.2 +++ b/src/HOL/Induct/README.html	Sun Nov 14 01:40:27 2004 +0100
    13.3 @@ -1,3 +1,5 @@
    13.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    13.5 +
    13.6  <!-- $Id$ -->
    13.7  <HTML><HEAD><TITLE>HOL/Induct/README</TITLE></HEAD><BODY>
    13.8  
    14.1 --- a/src/HOL/Isar_examples/README.html	Sat Nov 13 17:30:03 2004 +0100
    14.2 +++ b/src/HOL/Isar_examples/README.html	Sun Nov 14 01:40:27 2004 +0100
    14.3 @@ -1,3 +1,5 @@
    14.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    14.5 +
    14.6  <!-- $Id$ -->
    14.7  <html>
    14.8  
    15.1 --- a/src/HOL/Lambda/README.html	Sat Nov 13 17:30:03 2004 +0100
    15.2 +++ b/src/HOL/Lambda/README.html	Sun Nov 14 01:40:27 2004 +0100
    15.3 @@ -1,3 +1,5 @@
    15.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    15.5 +
    15.6  <!-- $Id$ -->
    15.7  <HTML><HEAD><TITLE>HOL/Lambda</TITLE></HEAD>
    15.8  <BODY>
    16.1 --- a/src/HOL/Library/README.html	Sat Nov 13 17:30:03 2004 +0100
    16.2 +++ b/src/HOL/Library/README.html	Sun Nov 14 01:40:27 2004 +0100
    16.3 @@ -1,3 +1,5 @@
    16.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    16.5 +
    16.6  <html>
    16.7  
    16.8  <!-- $Id$ -->
    17.1 --- a/src/HOL/Modelcheck/README.html	Sat Nov 13 17:30:03 2004 +0100
    17.2 +++ b/src/HOL/Modelcheck/README.html	Sun Nov 14 01:40:27 2004 +0100
    17.3 @@ -1,3 +1,5 @@
    17.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    17.5 +
    17.6  <html>
    17.7  
    17.8  <!-- $Id$ -->
    18.1 --- a/src/HOL/Prolog/README.html	Sat Nov 13 17:30:03 2004 +0100
    18.2 +++ b/src/HOL/Prolog/README.html	Sun Nov 14 01:40:27 2004 +0100
    18.3 @@ -1,3 +1,5 @@
    18.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    18.5 +
    18.6  <!-- $Id$ -->
    18.7  <HTML><HEAD>
    18.8  <TITLE>HOL/Prolog/README</TITLE>
    19.1 --- a/src/HOL/README.html	Sat Nov 13 17:30:03 2004 +0100
    19.2 +++ b/src/HOL/README.html	Sun Nov 14 01:40:27 2004 +0100
    19.3 @@ -1,3 +1,5 @@
    19.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    19.5 +
    19.6  <html>
    19.7  
    19.8  <!-- $Id$ -->
    20.1 --- a/src/HOL/Real/HahnBanach/README.html	Sat Nov 13 17:30:03 2004 +0100
    20.2 +++ b/src/HOL/Real/HahnBanach/README.html	Sun Nov 14 01:40:27 2004 +0100
    20.3 @@ -1,8 +1,10 @@
    20.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    20.5 +
    20.6  <HTML><HEAD><TITLE>HOL/Real/HahnBanach/README</TITLE></HEAD><BODY>
    20.7  
    20.8 -<H3> The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar).</H3>
    20.9 +<H3>The Hahn-Banach Theorem for Real Vector Spaces (Isabelle/Isar)</H3>
   20.10  
   20.11 -Author:     Gertrud Bauer, Technische Universit&auml;t M&uuml;nchen<P>
   20.12 +Author: Gertrud Bauer, Technische Universit&auml;t M&uuml;nchen<P>
   20.13  
   20.14  This directory contains the proof of the Hahn-Banach theorem for real vectorspaces,
   20.15  following H. Heuser, Funktionalanalysis, p. 228 -232.
    21.1 --- a/src/HOL/TLA/README.html	Sat Nov 13 17:30:03 2004 +0100
    21.2 +++ b/src/HOL/TLA/README.html	Sun Nov 14 01:40:27 2004 +0100
    21.3 @@ -1,3 +1,5 @@
    21.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    21.5 +
    21.6  <HTML><HEAD><TITLE>HOL/TLA</TITLE></HEAD><BODY>
    21.7  
    21.8  <H2>TLA: Lamport's Temporal Logic of Actions</H2>
    21.9 @@ -56,4 +58,4 @@
   21.10  <!-- hhmts start -->
   21.11  Last modified: Mon Jan 25 14:06:43 MET 1999
   21.12  <!-- hhmts end -->
   21.13 -</BODY></HTML>
   21.14 \ No newline at end of file
   21.15 +</BODY></HTML>
    22.1 --- a/src/HOL/Tools/refute.ML	Sat Nov 13 17:30:03 2004 +0100
    22.2 +++ b/src/HOL/Tools/refute.ML	Sun Nov 14 01:40:27 2004 +0100
    22.3 @@ -1141,11 +1141,11 @@
    22.4  			(* unit -> (interpretation * model * arguments) option *)
    22.5  			fun interpret_groundtype () =
    22.6  			let
    22.7 -				val size = (if T = Term.propT then 2 else (the o assoc) (typs, T))  (* the model MUST specify a size for ground types *)
    22.8 -				val next = (if size=2 then next_idx+1 else next_idx+size)  (* optimization for types with size 2 *)
    22.9 -				val _    = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ())  (* check if 'maxvars' is large enough *)
   22.10 +				val size = (if T = Term.propT then 2 else (the o assoc) (typs, T))                      (* the model MUST specify a size for ground types *)
   22.11 +				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 *)
   22.12 +				val _    = (if next-1>maxvars andalso maxvars>0 then raise MAXVARS_EXCEEDED else ())    (* check if 'maxvars' is large enough *)
   22.13  				(* prop_formula list *)
   22.14 -				val fms  = (if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
   22.15 +				val fms  = (if size=1 then [True] else if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
   22.16  					else (map BoolVar (next_idx upto (next_idx+size-1))))
   22.17  				(* interpretation *)
   22.18  				val intr = Leaf fms
   22.19 @@ -1155,7 +1155,7 @@
   22.20  				(* prop_formula list -> prop_formula *)
   22.21  				fun exactly_one_true xs = SAnd (PropLogic.exists xs, one_of_two_false xs)
   22.22  				(* prop_formula *)
   22.23 -				val wf   = (if size=2 then True else exactly_one_true fms)
   22.24 +				val wf   = (if size=1 then True else if size=2 then True else exactly_one_true fms)
   22.25  			in
   22.26  				(* extend the model, increase 'next_idx', add well-formedness condition *)
   22.27  				Some (intr, (typs, (t, intr)::terms), {maxvars = maxvars, next_idx = next, bounds = bounds, wellformed = SAnd (wellformed, wf)})
   22.28 @@ -1327,7 +1327,7 @@
   22.29  	in
   22.30  	(* ------------------------------------------------------------------------- *)
   22.31  	(* Providing interpretations directly is more efficient than unfolding the   *)
   22.32 -	(* logical constants.  IN HOL however, logical constants can themselves be   *)
   22.33 +	(* logical constants.  In HOL however, logical constants can themselves be   *)
   22.34  	(* arguments.  "All" and "Ex" are then translated just like any other        *)
   22.35  	(* constant, with the relevant axiom being added by 'collect_axioms'.        *)
   22.36  	(* ------------------------------------------------------------------------- *)
   22.37 @@ -1509,10 +1509,10 @@
   22.38  							(* recursively compute the size of the datatype *)
   22.39  							val size     = size_of_dtyp typs' descr typ_assoc constrs
   22.40  							val next_idx = #next_idx args
   22.41 -							val next     = (if size=2 then next_idx+1 else next_idx+size)  (* optimization for types with size 2 *)
   22.42 +							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 *)
   22.43  							val _        = (if next-1>(#maxvars args) andalso (#maxvars args)>0 then raise MAXVARS_EXCEEDED else ())  (* check if 'maxvars' is large enough *)
   22.44  							(* prop_formula list *)
   22.45 -							val fms      = (if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
   22.46 +							val fms      = (if size=1 then [True] else if size=2 then [BoolVar next_idx, Not (BoolVar next_idx)]
   22.47  								else (map BoolVar (next_idx upto (next_idx+size-1))))
   22.48  							(* interpretation *)
   22.49  							val intr     = Leaf fms
   22.50 @@ -1522,7 +1522,7 @@
   22.51  							(* prop_formula list -> prop_formula *)
   22.52  							fun exactly_one_true xs = SAnd (PropLogic.exists xs, one_of_two_false xs)
   22.53  							(* prop_formula *)
   22.54 -							val wf       = (if size=2 then True else exactly_one_true fms)
   22.55 +							val wf       = (if size=1 then True else if size=2 then True else exactly_one_true fms)
   22.56  						in
   22.57  							(* extend the model, increase 'next_idx', add well-formedness condition *)
   22.58  							Some (intr, (typs, (t, intr)::terms), {maxvars = #maxvars args, next_idx = next, bounds = #bounds args, wellformed = SAnd (#wellformed args, wf)})
    23.1 --- a/src/HOL/UNITY/Comp/README.html	Sat Nov 13 17:30:03 2004 +0100
    23.2 +++ b/src/HOL/UNITY/Comp/README.html	Sun Nov 14 01:40:27 2004 +0100
    23.3 @@ -1,3 +1,5 @@
    23.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    23.5 +
    23.6  <!-- $Id$ -->
    23.7  <HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
    23.8  
    24.1 --- a/src/HOL/UNITY/README.html	Sat Nov 13 17:30:03 2004 +0100
    24.2 +++ b/src/HOL/UNITY/README.html	Sun Nov 14 01:40:27 2004 +0100
    24.3 @@ -1,3 +1,5 @@
    24.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    24.5 +
    24.6  <!-- $Id$ -->
    24.7  <HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
    24.8  
    25.1 --- a/src/HOL/UNITY/Simple/README.html	Sat Nov 13 17:30:03 2004 +0100
    25.2 +++ b/src/HOL/UNITY/Simple/README.html	Sun Nov 14 01:40:27 2004 +0100
    25.3 @@ -1,3 +1,5 @@
    25.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    25.5 +
    25.6  <!-- $Id$ -->
    25.7  <HTML><HEAD><TITLE>HOL/UNITY/README</TITLE></HEAD><BODY>
    25.8  
    26.1 --- a/src/HOL/W0/README.html	Sat Nov 13 17:30:03 2004 +0100
    26.2 +++ b/src/HOL/W0/README.html	Sun Nov 14 01:40:27 2004 +0100
    26.3 @@ -1,3 +1,5 @@
    26.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    26.5 +
    26.6  <HTML><HEAD><TITLE>HOL/W0/README</TITLE></HEAD>
    26.7  <BODY>
    26.8  
    27.1 --- a/src/HOL/ex/README.html	Sat Nov 13 17:30:03 2004 +0100
    27.2 +++ b/src/HOL/ex/README.html	Sun Nov 14 01:40:27 2004 +0100
    27.3 @@ -1,3 +1,5 @@
    27.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    27.5 +
    27.6  <!-- $Id$ -->
    27.7  <HTML><HEAD><TITLE>HOL/ex/README</TITLE></HEAD><BODY>
    27.8  
    28.1 --- a/src/HOLCF/FOCUS/README.html	Sat Nov 13 17:30:03 2004 +0100
    28.2 +++ b/src/HOLCF/FOCUS/README.html	Sun Nov 14 01:40:27 2004 +0100
    28.3 @@ -1,3 +1,5 @@
    28.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    28.5 +
    28.6  <HTML><HEAD><TITLE>HOLCF/README</TITLE></HEAD><BODY>
    28.7  
    28.8  <H3>FOCUS: a theory of stream-processing functions Isabelle/<A HREF="..">HOLCF</A></H3>
    29.1 --- a/src/HOLCF/IMP/README.html	Sat Nov 13 17:30:03 2004 +0100
    29.2 +++ b/src/HOLCF/IMP/README.html	Sun Nov 14 01:40:27 2004 +0100
    29.3 @@ -1,8 +1,10 @@
    29.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    29.5 +
    29.6  <HTML><HEAD><TITLE>HOLCF/IMP/README</TITLE></HEAD><BODY>
    29.7  
    29.8 -<H2>IMP --- A <KBD>WHILE</KBD>-language and its Semantics</H2>
    29.9 +<H2>IMP -- A <KBD>WHILE</KBD>-language and its Semantics</H2>
   29.10  
   29.11  This is the HOLCF-based denotational semantics of a simple
   29.12 -<tt>WHILE</tt>-language. For a full description see <A
   29.13 -HREF="../../HOL/IMP/index.html"> HOL/IMP</A>.
   29.14 +<tt>WHILE</tt>-language.  For a full description see <A
   29.15 +HREF="../../HOL/IMP/index.html">HOL/IMP</A>.
   29.16  </BODY></HTML>
    30.1 --- a/src/HOLCF/IOA/README.html	Sat Nov 13 17:30:03 2004 +0100
    30.2 +++ b/src/HOLCF/IOA/README.html	Sun Nov 14 01:40:27 2004 +0100
    30.3 @@ -1,3 +1,5 @@
    30.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    30.5 +
    30.6  <HTML><HEAD><TITLE>HOLCF/IOA/README</TITLE></HEAD><BODY>
    30.7  
    30.8  <H3>IOA: A formalization of I/O automata in HOLCF</H3>
    31.1 --- a/src/HOLCF/README.html	Sat Nov 13 17:30:03 2004 +0100
    31.2 +++ b/src/HOLCF/README.html	Sun Nov 14 01:40:27 2004 +0100
    31.3 @@ -1,3 +1,5 @@
    31.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    31.5 +
    31.6  <HTML><HEAD><TITLE>HOLCF/README</TITLE></HEAD><BODY>
    31.7  
    31.8  <H3>HOLCF: A higher-order version of LCF based on Isabelle/HOL</H3>
    32.1 --- a/src/LCF/README.html	Sat Nov 13 17:30:03 2004 +0100
    32.2 +++ b/src/LCF/README.html	Sun Nov 14 01:40:27 2004 +0100
    32.3 @@ -1,3 +1,5 @@
    32.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    32.5 +
    32.6  <HTML><HEAD><TITLE>LCF/README</TITLE></HEAD><BODY>
    32.7  
    32.8  <H2>LCF: Logic for Computable Functions</H2>
    33.1 --- a/src/Sequents/README.html	Sat Nov 13 17:30:03 2004 +0100
    33.2 +++ b/src/Sequents/README.html	Sun Nov 14 01:40:27 2004 +0100
    33.3 @@ -1,3 +1,5 @@
    33.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    33.5 +
    33.6  <!-- $Id$ -->
    33.7  <HTML><HEAD><TITLE>Sequents/README</TITLE></HEAD><BODY>
    33.8  
    34.1 --- a/src/ZF/AC/README.html	Sat Nov 13 17:30:03 2004 +0100
    34.2 +++ b/src/ZF/AC/README.html	Sun Nov 14 01:40:27 2004 +0100
    34.3 @@ -1,3 +1,5 @@
    34.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    34.5 +
    34.6  <!-- $Id$ -->
    34.7  <HTML><HEAD><TITLE>ZF/AC/README</TITLE></HEAD><BODY>
    34.8  
    34.9 @@ -16,7 +18,9 @@
   34.10  
   34.11  <P>
   34.12  The report
   34.13 -<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.
   34.14 +<A HREF="http://www.cl.cam.ac.uk/Research/Reports/TR377-lcp-mechanising-set-theory.ps.gz">Mechanizing Set Theory</A>,
   34.15 +by Paulson and Grabczewski, describes both this development and ZF's theories
   34.16 +of cardinals.
   34.17  
   34.18  </body>
   34.19  </html>
    35.1 --- a/src/ZF/Coind/README.html	Sat Nov 13 17:30:03 2004 +0100
    35.2 +++ b/src/ZF/Coind/README.html	Sun Nov 14 01:40:27 2004 +0100
    35.3 @@ -1,3 +1,5 @@
    35.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    35.5 +
    35.6  <!-- $Id$ -->
    35.7  <HTML><HEAD><TITLE>ZF/Coind/README</TITLE></HEAD><BODY>
    35.8  
    36.1 --- a/src/ZF/Constructible/README.html	Sat Nov 13 17:30:03 2004 +0100
    36.2 +++ b/src/ZF/Constructible/README.html	Sun Nov 14 01:40:27 2004 +0100
    36.3 @@ -1,8 +1,10 @@
    36.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    36.5 +
    36.6  <HTML><HEAD><TITLE>ZF/Constructible/README</TITLE></HEAD><BODY>
    36.7  
    36.8  <H1>Constructible--Relative Consistency of the Axiom of Choice</H1>
    36.9  
   36.10 -<P>Gödel's proof of the relative consistency of the axiom of choice is
   36.11 +<P>G&ouml;del's proof of the relative consistency of the axiom of choice is
   36.12  mechanized using Isabelle/ZF.  The proof builds upon a previous mechanization
   36.13  of the
   36.14  <A HREF="http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf">reflection
   36.15 @@ -25,4 +27,4 @@
   36.16  HREF="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</A>,
   36.17  <A HREF="mailto:lcp@cl.cam.ac.uk">lcp@cl.cam.ac.uk</A>
   36.18  </ADDRESS>
   36.19 -</BODY></HTML>
   36.20 \ No newline at end of file
   36.21 +</BODY></HTML>
    37.1 --- a/src/ZF/IMP/README.html	Sat Nov 13 17:30:03 2004 +0100
    37.2 +++ b/src/ZF/IMP/README.html	Sun Nov 14 01:40:27 2004 +0100
    37.3 @@ -1,12 +1,13 @@
    37.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    37.5 +
    37.6  <!-- $Id$ -->
    37.7  <HTML><HEAD><TITLE>ZF/IMP/README</TITLE></HEAD><BODY>
    37.8  
    37.9  <H2>IMP -- A <KBD>while</KBD>-language and two semantics</H2>
   37.10  
   37.11 -The formalization of the denotational and operational semantics of
   37.12 -a simple while-language together with an equivalence proof between the two
   37.13 -semantics. The whole development essentially formalizes/transcribes chapters
   37.14 -2 and 5 of
   37.15 +The formalization of the denotational and operational semantics of a simple
   37.16 +while-language together with an equivalence proof between the two semantics.
   37.17 +The whole development essentially formalizes/transcribes chapters 2 and 5 of
   37.18  <P>
   37.19  <PRE>
   37.20  @book{Winskel,
   37.21 @@ -16,9 +17,9 @@
   37.22   year = 1993}.
   37.23  </PRE>
   37.24  <P>
   37.25 -There is a 
   37.26 -<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/loetz-sand.dvi.gz">
   37.27 -report</A> by Lötzbeyer and Sandner.
   37.28 +There is a
   37.29 +<A HREF="http://www4.informatik.tu-muenchen.de/~nipkow/pubs/loetz-sand.dvi.gz">report</A>
   37.30 +by L&ouml;tzbeyer and Sandner.
   37.31  <P>
   37.32  A much extended version of this development is found in
   37.33  <A HREF="../../HOL/IMP/index.html">HOL/IMP</A>.
    38.1 --- a/src/ZF/README.html	Sat Nov 13 17:30:03 2004 +0100
    38.2 +++ b/src/ZF/README.html	Sun Nov 14 01:40:27 2004 +0100
    38.3 @@ -1,3 +1,5 @@
    38.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    38.5 +
    38.6  <HTML><HEAD><TITLE>ZF/README</TITLE></HEAD><BODY>
    38.7  
    38.8  <H2>ZF: Zermelo-Fraenkel Set Theory</H2>
    38.9 @@ -23,7 +25,7 @@
   38.10  
   38.11  <DT>Resid
   38.12  <DD>subdirectory containing a proof of the Church-Rosser Theorem.  It is
   38.13 -by Ole Rasmussen, following the Coq proof by Gérard Huet.<P>
   38.14 +by Ole Rasmussen, following the Coq proof by G�ard Huet.<P>
   38.15  
   38.16  <DT>ex
   38.17  <DD>subdirectory containing various examples.
    39.1 --- a/src/ZF/Resid/README.html	Sat Nov 13 17:30:03 2004 +0100
    39.2 +++ b/src/ZF/Resid/README.html	Sun Nov 14 01:40:27 2004 +0100
    39.3 @@ -1,3 +1,5 @@
    39.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    39.5 +
    39.6  <!-- $Id$ -->
    39.7  <HTML><HEAD><TITLE>ZF/Resid/README</TITLE></HEAD><BODY>
    39.8  
    40.1 --- a/src/ZF/ex/README.html	Sat Nov 13 17:30:03 2004 +0100
    40.2 +++ b/src/ZF/ex/README.html	Sun Nov 14 01:40:27 2004 +0100
    40.3 @@ -1,3 +1,5 @@
    40.4 +<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN" "http://www.w3.org/TR/html4/loose.dtd">
    40.5 +
    40.6  <!-- $Id$ -->
    40.7  <HTML><HEAD><TITLE>ZF/ex/README</TITLE></HEAD><BODY>
    40.8