--- a/Admin/makedist Fri May 05 22:23:27 2000 +0200
+++ b/Admin/makedist Fri May 05 22:24:03 2000 +0200
@@ -157,7 +157,7 @@
} >UNOFFICIAL
fi
-perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index1.html lib/html/index2.html
+perl -pi -e "s/{ISABELLE}/$DISTNAME/g;" lib/html/index.html
perl -pi -e "s/Isabelle repository/$DISTVERSION/" src/Pure/ROOT.ML
perl -pi -e "s/the internal repository version of Isabelle/$DISTVERSION/" README.html
lynx -dump README.html >README
--- a/lib/Tools/usedir Fri May 05 22:23:27 2000 +0200
+++ b/lib/Tools/usedir Fri May 05 22:24:03 2000 +0200
@@ -106,18 +106,15 @@
# prepare browser info dir
if [ "$INFO" = "true" -a ! -f $ISABELLE_BROWSER_INFO/index.html ]; then
-
mkdir -p $ISABELLE_BROWSER_INFO
cp $ISABELLE_HOME/lib/logo/isabelle.gif $ISABELLE_BROWSER_INFO/isabelle.gif
- cp $ISABELLE_HOME/lib/html/index1.html $ISABELLE_BROWSER_INFO/index.html
+ cp $ISABELLE_HOME/lib/html/index.html $ISABELLE_BROWSER_INFO/index.html
mkdir -p $ISABELLE_BROWSER_INFO/graph
- cp $ISABELLE_HOME/lib/html/index2.html $ISABELLE_BROWSER_INFO/graph/index.html
mkdir $ISABELLE_BROWSER_INFO/graph/GraphBrowser
mkdir $ISABELLE_BROWSER_INFO/graph/awtUtilities
cp $ISABELLE_HOME/lib/browser/GraphBrowser/*.class $ISABELLE_BROWSER_INFO/graph/GraphBrowser
cp $ISABELLE_HOME/lib/browser/awtUtilities/*.class $ISABELLE_BROWSER_INFO/graph/awtUtilities
-
fi
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/lib/html/index.html Fri May 05 22:24:03 2000 +0200
@@ -0,0 +1,60 @@
+<html>
+
+<head><title>The Isabelle Library ({ISABELLE})</title></head>
+
+<body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040">
+
+<center>
+ <table width="100%" border="0" cellspacing="10" cellpadding="0">
+ <tr>
+ <td width="20%" valign="middle" align="center">
+ <img align=bottom src="isabelle.gif" width="100" height="86" alt="[Isabelle]">
+ </td>
+ <td width="80%" valign="middle" align="center">
+ <table width="90%" border="0" cellspacing="0" cellpadding="20">
+ <tr>
+ <td valign="middle" align="center" bgcolor="#aacccc">
+ <font face="Helvetica,Arial" size="+2">The Isabelle Library</font>
+ </td>
+ </tr>
+ </table>
+ </td>
+ </tr>
+ </table>
+</center>
+
+<hr>
+
+Higher-Order Logic
+
+<ul>
+<li><a href="HOL/index.html"> HOL (Simply-typed Set Theory)</a>
+<li><a href="HOLCF/index.html">HOLCF (Higher-Order Logic of Computable Functions)</a>
+</ul>
+
+<hr>
+
+First-Order Logic
+
+<ul>
+<li><a href="FOL/index.html">FOL (Many-sorted First-Order Logic)</a>
+<li><a href="ZF/index.html">ZF (Set Theory)</a>
+<li><a href="CCL/index.html">CCL (Classical Computational Logic)</a>
+<li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a>
+<li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a>
+</ul>
+
+<hr>
+
+Miscellaneous
+
+<ul>
+<li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a>
+<li><a href="CTT/index.html">CTT (Constructive Type Theory)</a>
+<li><a href="Cube/index.html">Cube (The Lambda Cube)</a>
+</ul>
+
+<hr>
+
+</body>
+</html>
--- a/lib/html/index1.html Fri May 05 22:23:27 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-<html>
-
-<head><title>Isabelle Logics ({ISABELLE})</title></head>
-
-<body>
-
-<center><img src="isabelle.gif" alt="Isabelle"></center>
-
-<p>
-
-Switch to <a href="graph/index.html">Java-based</a> version, including
-theory graph browser.
-
-<p>
-
-Click on the logic's name to view a list of its theories.
-
-<hr>
-
-First-Order Logic
-
-<ul>
-<li><a href="FOL/index.html">FOL</a>
-<li><a href="ZF/index.html">ZF (Set Theory)</a>
-<li><a href="CCL/index.html">CCL (Classical Computational Logic)</a>
-<li><a href="LCF/index.html">LCF (Logic of Computable Functions)</a>
-<li><a href="FOLP/index.html">FOLP (FOL with Proof Terms)</a>
-</ul>
-
-<hr>
-
-Higher-Order Logic
-
-<ul>
-<li><a href="HOL/index.html">HOL</a>
-<li><a href="HOLCF/index.html">HOLCF (Higher-Order Logic of Computable Functions)</a>
-</ul>
-
-<hr>
-
-Miscellaneous
-
-<ul>
-<li><a href="Sequents/index.html">Sequents (first-order, modal and linear logics)</a>
-<li><a href="CTT/index.html">CTT (Constructive Type Theory)</a>
-<li><a href="Cube/index.html">Cube (The Lambda Cube)</a>
-</ul>
-
-<hr>
-
-</body>
-</html>
--- a/lib/html/index2.html Fri May 05 22:23:27 2000 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,51 +0,0 @@
-<html>
-
-<head><title>Isabelle Logics ({ISABELLE})</title></head>
-
-<body>
-
-<center><img src="../isabelle.gif" alt="Isabelle"></center>
-
-<p>
-
-Switch to <a href="../index.html">plain HTML</a> version.
-
-<p>
-
-Click on the logic's name to view the graph of its theories.
-
-<hr>
-
-First-Order Logic
-
-<ul>
-<li><a href="data/FOL/medium.html">FOL</a>
-<li><a href="data/ZF/medium.html">ZF (Set Theory)</a>
-<li><a href="data/CCL/medium.html">CCL (Classical Computational Logic)</a>
-<li><a href="data/LCF/medium.html">LCF (Logic of Computable Functions)</a>
-<li><a href="data/FOLP/medium.html">FOLP (FOL with Proof Terms)</a>
-</ul>
-
-<hr>
-
-Higher-Order Logic
-
-<ul>
-<li><a href="data/HOL/medium.html">HOL</a>
-<li><a href="data/HOLCF/medium.html">HOLCF (Higher-Order Logic of Computable Functions)</a>
-</ul>
-
-<hr>
-
-Miscellaneous
-
-<ul>
-<li><a href="data/Sequents/medium.html">Sequents (first-order, modal and linear logics)</a>
-<li><a href="data/CTT/medium.html">CTT (Constructive Type Theory)</a>
-<li><a href="data/Cube/medium.html">Cube (The Lambda Cube)</a>
-</ul>
-
-<hr>
-
-</body>
-</html>