Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/ZF/Constructible/README.html
changeset 15582 7219facb3fd0
parent 15283 f21466450330
child 36862 952b2b102a0a 
--- 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 @@
 <!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>
+<!-- $Id$ -->
+
+<html>
 
-<H1>Constructible--Relative Consistency of the Axiom of Choice</H1>
+<head>
+  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+  <title>ZF/Constructible/README</title>
+</head>
 
-<P>G&ouml;del's proof of the relative consistency of the axiom of choice is
+<body>
+<h1>Constructible--Relative Consistency of the Axiom of Choice</h1>
+
+G&ouml;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
-theorem</A>.  The heavy reliance on metatheory in the original proof makes the
+<a href="http://www.cl.cam.ac.uk/users/lcp/papers/Sets/reflection.pdf">reflection
+theorem</a>.  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 <STRONG>Set Theory</STRONG>, and could support the
+a standard textbook, Kunen's <strong>Set Theory</strong>, 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
-<A HREF="http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf">available</A>.
+<a href="http://www.cl.cam.ac.uk/TechReports/UCAM-CL-TR-551.pdf">available</a>.
 
-<HR>
-<P>Last modified $Date$
+<hr>
+
+<p>
 
-<ADDRESS>
-<A
-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>
+Last modified $Date$
+
+<address>
+<a 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>
isabelle