weblinted, tuned;
authorwenzelm
Thu Aug 27 11:50:18 1998 +0200 (1998-08-27)
changeset 538374c2da44d144
parent 5382 dfbe72ddbd2d
child 5384 c974451df466
weblinted, tuned;
lib/html/index1.html
lib/html/index2.html
src/HOL/TLA/README.html
src/Sequents/README.html
src/ZF/ex/README.html
     1.1 --- a/lib/html/index1.html	Thu Aug 27 11:19:35 1998 +0200
     1.2 +++ b/lib/html/index1.html	Thu Aug 27 11:50:18 1998 +0200
     1.3 @@ -1,34 +1,52 @@
     1.4 -<HTML><HEAD><TITLE>Isabelle Logics ({ISABELLE})</TITLE></HEAD>
     1.5 -<center>
     1.6 - <img src="gif/isabelle.gif"><P>
     1.7 -</center>
     1.8 -<P>
     1.9 -Switch to <A HREF="graph/index.html">Java-based</A> version, including theory graph browser.
    1.10 -<P>
    1.11 +<html>
    1.12 +
    1.13 +<head><title>Isabelle Logics ({ISABELLE})</title></head>
    1.14 +
    1.15 +<body>
    1.16 +
    1.17 +<img src="gif/isabelle.gif" alt="Isabelle" align=center>
    1.18 +
    1.19 +<p>
    1.20 +
    1.21 +Switch to <a href="graph/index.html">Java-based</a> version, including
    1.22 +theory graph browser.
    1.23 +
    1.24 +<p>
    1.25 +
    1.26  Click on the logic's name to view a list of its theories.
    1.27 -<HR>
    1.28 +
    1.29 +<hr>
    1.30 +
    1.31  First-Order Logic
    1.32 -  <UL>
    1.33 -  <LI><A HREF = "FOL/index.html">FOL</A>
    1.34 -  <LI><A HREF = "ZF/index.html">ZF (Set Theory)</A>
    1.35 -  <LI><A HREF = "CCL/index.html">CCL (Classical Computational Logic)</A>
    1.36 -  <LI><A HREF = "LCF/index.html">LCF (Logic of Computable Functions)</A>
    1.37 -  <LI><A HREF = "FOLP/index.html">FOLP (FOL with Proof Terms)</A>
    1.38 -  </UL>
    1.39 -<HR>
    1.40 +
    1.41 +<ul>
    1.42 +<li><a href="FOL/index.html">FOL</a>
    1.43 +<li><a href="ZF/index.html">ZF (Set Theory)</a>
    1.44 +<li><a href="CCL/index.html">CCL (Classical Computational Logic)</a>
    1.45 +<li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a>
    1.46 +<li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a>
    1.47 +</ul>
    1.48 +
    1.49 +<hr>
    1.50 +
    1.51  Higher-Order Logic
    1.52 -  <UL>
    1.53 -  <LI><A HREF = "HOL/index.html">HOL</A>
    1.54 -  <LI><A HREF = "HOLCF/index.html">HOLCF 
    1.55 -		   (Higher-Order Logic of Computable Functions)</A>
    1.56 -  </UL>
    1.57 -<HR>
    1.58 +
    1.59 +<ul>
    1.60 +<li><a href="HOL/index.html">HOL</a>
    1.61 +<li><a href="HOLCF/index.html">HOLCF (Higher-Order Logic of Computable Functions)</a>
    1.62 +</ul>
    1.63 +
    1.64 +<hr>
    1.65 +
    1.66  Miscellaneous
    1.67 -  <UL>
    1.68 -  <LI><A HREF = "Sequents/index.html">Sequents 
    1.69 -	  (first-order, modal and linear logics)</A>
    1.70 -  <LI><A HREF = "CTT/index.html">CTT (Constructive Type Theory)</A>
    1.71 -  <LI><A HREF = "Cube/index.html">Cube (The Lambda Cube)</A>
    1.72 -  </UL>
    1.73 -<HR>
    1.74 -</BODY></HTML>
    1.75 +
    1.76 +<ul>
    1.77 +<li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a>
    1.78 +<li><a href="CTT/index.html">CTT (Constructive Type Theory)</a>
    1.79 +<li><a href="Cube/index.html">Cube (The Lambda Cube)</a>
    1.80 +</ul>
    1.81 +
    1.82 +<hr>
    1.83 +
    1.84 +</body>
    1.85 +</html>
     2.1 --- a/lib/html/index2.html	Thu Aug 27 11:19:35 1998 +0200
     2.2 +++ b/lib/html/index2.html	Thu Aug 27 11:50:18 1998 +0200
     2.3 @@ -1,34 +1,51 @@
     2.4 -<HTML><HEAD><TITLE>Isabelle Logics ({ISABELLE})</TITLE></HEAD>
     2.5 -<center>
     2.6 - <img src="../gif/isabelle.gif"><P>
     2.7 -</center>
     2.8 -<P>
     2.9 -Switch to <A HREF="../index.html">plain HTML</A> version.
    2.10 -<P>
    2.11 +<html>
    2.12 +
    2.13 +<head><title>Isabelle Logics ({ISABELLE})</title></head>
    2.14 +
    2.15 +<body>
    2.16 +
    2.17 +<img src="../gif/isabelle.gif" alt="Isabelle" align=center>
    2.18 +
    2.19 +<p>
    2.20 +
    2.21 +Switch to <a href="../index.html">plain HTML</a> version.
    2.22 +
    2.23 +<p>
    2.24 +
    2.25  Click on the logic's name to view the graph of its theories.
    2.26 -<HR>
    2.27 +
    2.28 +<hr>
    2.29 +
    2.30  First-Order Logic
    2.31 -  <UL>
    2.32 -  <LI><A HREF = "data/FOL/large.html">FOL</A>
    2.33 -  <LI><A HREF = "data/ZF/large.html">ZF (Set Theory)</A>
    2.34 -  <LI><A HREF = "data/CCL/large.html">CCL (Classical Computational Logic)</A>
    2.35 -  <LI><A HREF = "data/LCF/large.html">LCF (Logic of Computable Functions)</A>
    2.36 -  <LI><A HREF = "data/FOLP/large.html">FOLP (FOL with Proof Terms)</A>
    2.37 -  </UL>
    2.38 -<HR>
    2.39 +
    2.40 +<ul>
    2.41 +<li><a href="data/FOL/large.html">FOL</a>
    2.42 +<li><a href="data/ZF/large.html">ZF (Set Theory)</a>
    2.43 +<li><a href="data/CCL/large.html">CCL (Classical Computational Logic)</a>
    2.44 +<li><a href="data/LCF/large.html">LCF (Logic of Computable Functions)</a>
    2.45 +<li><a href="data/FOLP/large.html">FOLP (FOL with Proof Terms)</a>
    2.46 +</ul>
    2.47 +
    2.48 +<hr>
    2.49 +
    2.50  Higher-Order Logic
    2.51 -  <UL>
    2.52 -  <LI><A HREF = "data/HOL/large.html">HOL</A>
    2.53 -  <LI><A HREF = "data/HOLCF/large.html">HOLCF 
    2.54 -		   (Higher-Order Logic of Computable Functions)</A>
    2.55 -  </UL>
    2.56 -<HR>
    2.57 +
    2.58 +<ul>
    2.59 +<li><a href="data/HOL/large.html">HOL</a>
    2.60 +<li><a href="data/HOLCF/large.html">HOLCF (Higher-Order Logic of Computable Functions)</a>
    2.61 +</ul>
    2.62 +
    2.63 +<hr>
    2.64 +
    2.65  Miscellaneous
    2.66 -  <UL>
    2.67 -  <LI><A HREF = "data/Sequents/large.html">Sequents 
    2.68 -	  (first-order, modal and linear logics)</A>
    2.69 -  <LI><A HREF = "data/CTT/large.html">CTT (Constructive Type Theory)</A>
    2.70 -  <LI><A HREF = "data/Cube/large.html">Cube (The Lambda Cube)</A>
    2.71 -  </UL>
    2.72 -<HR>
    2.73 -</BODY></HTML>
    2.74 +
    2.75 +<ul>
    2.76 +<li><a href="data/Sequents/large.html">Sequents (first-order, modal and linear logics)</a>
    2.77 +<li><a href="data/CTT/large.html">CTT (Constructive Type Theory)</a>
    2.78 +<li><a href="data/Cube/large.html">Cube (The Lambda Cube)</a>
    2.79 +</ul>
    2.80 +
    2.81 +<hr>
    2.82 +
    2.83 +</body>
    2.84 +</html>
     3.1 --- a/src/HOL/TLA/README.html	Thu Aug 27 11:19:35 1998 +0200
     3.2 +++ b/src/HOL/TLA/README.html	Thu Aug 27 11:50:18 1998 +0200
     3.3 @@ -26,7 +26,7 @@
     3.4  
     3.5  The distribution includes the following examples:
     3.6  <UL>
     3.7 -  <li> a verification of Lamport's <quote>increment</quote> example
     3.8 +  <li> a verification of Lamport's <em>increment</em> example
     3.9    (subdirectory inc),<P>
    3.10  
    3.11    <li> a proof that two buffers in a row implement a single buffer
     4.1 --- a/src/Sequents/README.html	Thu Aug 27 11:19:35 1998 +0200
     4.2 +++ b/src/Sequents/README.html	Thu Aug 27 11:50:18 1998 +0200
     4.3 @@ -41,5 +41,5 @@
     4.4      Linear Logic in Isabelle (in TR 379, University of Cambridge
     4.5  				Computer Lab, 1995, ed L. Paulson)
     4.6  </UL>
     4.7 -</UL>
     4.8 +
     4.9  </BODY></HTML>
     5.1 --- a/src/ZF/ex/README.html	Thu Aug 27 11:19:35 1998 +0200
     5.2 +++ b/src/ZF/ex/README.html	Thu Aug 27 11:50:18 1998 +0200
     5.3 @@ -5,7 +5,7 @@
     5.4  
     5.5  <P>Examples on this directory include a simple form of Ramsey's theorem.  A
     5.6  <A
     5.7 -HREF="http://www.cl.cam.ac.uk/Research/Reports/TR271-lcp-set-theory.dvi.Z"">report</A>
     5.8 +HREF="http://www.cl.cam.ac.uk/Research/Reports/TR271-lcp-set-theory.dvi.Z">report</A>
     5.9  is available.
    5.10  
    5.11  <P>Several (co)inductive and (co)datatype definitions are presented.  <A HREF="http://www.cl.cam.ac.uk/Research/Reports/TR312-lcp-set-II.ps.gz">One report</A> describes the theoretical foundations of datatypes while <A HREF="http://www.cl.cam.ac.uk/Research/Reports/TR320-lcp-isabelle-ind-defs.dvi.gz">another</A> describes the package that automates their declaration.