--- a/ANNOUNCE Tue Feb 13 16:05:56 2001 +0100
+++ b/ANNOUNCE Tue Feb 13 16:31:18 2001 +0100
@@ -12,22 +12,22 @@
* Poly/ML 4.0 used by default
More robust, less disk space required.
- * Pure/Simplifier (Stefan Berghofer)
+ * Simplifier (Stefan Berghofer)
Proper implementation as a derived rule, outside the kernel!
+ * Improved document preparation (Markus Wenzel)
+ Near math-mode, sub/super scripts, more symbols etc.
+
* Isabelle/Isar (Markus Wenzel)
Numerous usability improvements, e.g. support for initial
schematic goals, failure prediction of subgoal statements,
handling of non-atomic statements in induction.
- * Improved document preparation (Markus Wenzel)
- Near math-mode, sub/super scripts, more symbols etc.
-
* HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson,
Thomas M Rasmussen, Markus Wenzel)
A collection of generic theories to be used together with main HOL.
- * HOL/Real and HOL/Hyperreal (Jacques Fleuriot and Lawrence C Paulson)
+ * HOL/Real and HOL/Hyperreal (Jacques Fleuriot, Lawrence C Paulson)
General cleanup, more on nonstandard real analysis.
* HOL/Unix (Markus Wenzel)
--- a/Admin/page/dist-content/docs.content Tue Feb 13 16:05:56 2001 +0100
+++ b/Admin/page/dist-content/docs.content Tue Feb 13 16:31:18 2001 +0100
@@ -13,10 +13,10 @@
information about the present release and additional installation
instructions.
<ul>
-<li> <!-- _GP_ href(distname . "/ANNOUNCE", "ANNOUNCE") -->
-<li> <!-- _GP_ href(distname . "/README.html", "README") -->
-<li> <!-- _GP_ href(distname . "/INSTALL", "INSTALL") -->
-<li> <!-- _GP_ href(distname . "/NEWS", "NEWS") -->
+<li><!-- _GP_ href(distname . "/ANNOUNCE", "ANNOUNCE") -->
+<li><!-- _GP_ href(distname . "/README.html", "README") -->
+<li><!-- _GP_ href(distname . "/INSTALL", "INSTALL") -->
+<li><!-- _GP_ href(distname . "/NEWS", "NEWS") -->
</ul>
<p>
--- a/Admin/page/dist-content/index.content Tue Feb 13 16:05:56 2001 +0100
+++ b/Admin/page/dist-content/index.content Tue Feb 13 16:31:18 2001 +0100
@@ -11,18 +11,18 @@
<ul>
-<li> <a
+<li><a
href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/packages.html">Cambridge
(UK)</a>
-<li> <a href="http://isabelle.in.tum.de/dist/packages.html">Munich
+<li><a href="http://isabelle.in.tum.de/dist/packages.html">Munich
(Germany)</a>
-<li> <a
+<li><a
href="http://ftp.research.bell-labs.com/dist/smlnj/isabelle/packages.html">New
Jersey (USA)</a>
-<li> <a
+<li><a
href="ftp://rodin.stanford.edu/pub/smlnj/isabelle/packages.html">Stanford
(USA)</a>
--- a/Admin/page/dist-content/past.content Tue Feb 13 16:05:56 2001 +0100
+++ b/Admin/page/dist-content/past.content Tue Feb 13 16:31:18 2001 +0100
@@ -7,12 +7,13 @@
Past releases of Isabelle are available from the Cambrige ftp archive:
<ul>
-<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle99.tar.gz">Isabelle99</a> </li>
-<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle98-1.tar.gz">Isabelle98-1</a> </li>
-<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle98.tar.gz">Isabelle98</a> </li>
-<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-8.tar.gz">Isabelle94-8</a> </li>
-<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-7.tar.gz">Isabelle94-7</a> </li>
-<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-6.tar.gz">Isabelle94-6</a> </li>
-<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94.tar.gz">Isabelle94</a> </li>
-<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle93.tar.gz">Isabelle93</a> </li>
+<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle99-1.tar.gz">Isabelle99</a></li>
+<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle99.tar.gz">Isabelle99</a></li>
+<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle98-1.tar.gz">Isabelle98-1</a></li>
+<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle98.tar.gz">Isabelle98</a></li>
+<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-8.tar.gz">Isabelle94-8</a></li>
+<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-7.tar.gz">Isabelle94-7</a></li>
+<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-6.tar.gz">Isabelle94-6</a></li>
+<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94.tar.gz">Isabelle94</a></li>
+<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle93.tar.gz">Isabelle93</a></li>
</ul>
--- a/Admin/page/main-content/index.content Tue Feb 13 16:05:56 2001 +0100
+++ b/Admin/page/main-content/index.content Tue Feb 13 16:31:18 2001 +0100
@@ -19,11 +19,12 @@
<ul>
-<li> <a
+<li><a
href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle
-at Cambridge</strong></a>
+at Cambridge</strong></a>
-<li> <a href="http://isabelle.in.tum.de/munich.html"><strong>Isabelle at Munich</strong></a>
+<li><a href="http://isabelle.in.tum.de/munich.html"><strong>Isabelle
+at Munich</strong></a>
</ul>
--- a/Admin/page/main-content/logics.content Tue Feb 13 16:05:56 2001 +0100
+++ b/Admin/page/main-content/logics.content Tue Feb 13 16:31:18 2001 +0100
@@ -79,16 +79,16 @@
<ol>
-<li> declare concrete syntax (via mixfix grammar and syntax macros),
+<li>declare concrete syntax (via mixfix grammar and syntax macros),
-<li> declare abstract syntax (as higher-order constants),
+<li>declare abstract syntax (as higher-order constants),
-<li> declare inference rules (as meta-logical propositions),
+<li>declare inference rules (as meta-logical propositions),
-<li> instantiate generic automatic proof tools (simplifier, classical
+<li>instantiate generic automatic proof tools (simplifier, classical
tableau prover etc.),
-<li> manually code special proof procedures (via tacticals or
+<li>manually code special proof procedures (via tacticals or
hand-written ML).
</ol>
--- a/Admin/page/main-content/munich.content Tue Feb 13 16:05:56 2001 +0100
+++ b/Admin/page/main-content/munich.content Tue Feb 13 16:31:18 2001 +0100
@@ -24,16 +24,16 @@
<ul>
-<li> <a href="http://www.in.tum.de/~bauerg/">Gertrud Bauer</a>
-<li> <a href="http://www4.in.tum.de/~berghofe/">Stefan Berghofer</a>
-<li> <a href="http://www4.in.tum.de/~kleing/">Gerwin Klein</a>
-<li> <a href="http://www4.in.tum.de/~narasche/">Wolfgang Naraschewski</a>
-<li> <a href="http://www4.in.tum.de/~nipkow/">Tobias Nipkow</a>
-<li> <a href="http://www4.in.tum.de/~oheimb/">David von Oheimb</a>
-<li> <a href="http://www4.in.tum.de/~prensani/">Leonor Prensa Nieto</a>
-<li> <a href="http://www4.in.tum.de/~pusch/">Cornelia Pusch</a>
-<li> <a href="http://www4.in.tum.de/~streckem/">Martin Strecker</a>
-<li> <a href="http://www4.in.tum.de/~wenzelm/">Markus Wenzel</a>
+<li><a href="http://www.in.tum.de/~bauerg/">Gertrud Bauer</a>
+<li><a href="http://www4.in.tum.de/~berghofe/">Stefan Berghofer</a>
+<li><a href="http://www4.in.tum.de/~kleing/">Gerwin Klein</a>
+<li><a href="http://www4.in.tum.de/~narasche/">Wolfgang Naraschewski</a>
+<li><a href="http://www4.in.tum.de/~nipkow/">Tobias Nipkow</a>
+<li><a href="http://www4.in.tum.de/~oheimb/">David von Oheimb</a>
+<li><a href="http://www4.in.tum.de/~prensani/">Leonor Prensa Nieto</a>
+<li><a href="http://www4.in.tum.de/~pusch/">Cornelia Pusch</a>
+<li><a href="http://www4.in.tum.de/~streckem/">Martin Strecker</a>
+<li><a href="http://www4.in.tum.de/~wenzelm/">Markus Wenzel</a>
</ul>
@@ -42,10 +42,10 @@
<ul>
-<li> <a href="mailto:buttenbe@in.tum.de">Christian Buttenberg</a> </li>
-<li> <a href="http://home.informatik.tu-muenchen.de/~kirsch/">Alexandra Kirsch</a> </li>
-<li> <a href="http://www.informatik.tu-muenchen.de/~nanz/">Sebastian Nanz</a> </li>
-<li> <a href="http://www.informatik.tu-muenchen.de/~pfeifrot/">Johannes Pfeifroth</a> </li>
+<li><a href="mailto:buttenbe@in.tum.de">Christian Buttenberg</a> </li>
+<li><a href="http://home.informatik.tu-muenchen.de/~kirsch/">Alexandra Kirsch</a> </li>
+<li><a href="http://www.informatik.tu-muenchen.de/~nanz/">Sebastian Nanz</a> </li>
+<li><a href="http://www.informatik.tu-muenchen.de/~pfeifrot/">Johannes Pfeifroth</a> </li>
</ul>
@@ -56,20 +56,20 @@
<ul>
-<li> <b><a href="Bali/index.html">Isabelle/Bali</a></b> Java and JVM
+<li><b><a href="Bali/index.html">Isabelle/Bali</a></b> Java and JVM
formalization --- type system, semantics, compilers
-<li> <b><a href="Isar/index.html">Isabelle/Isar</a></b> Intelligible
+<li><b><a href="Isar/index.html">Isabelle/Isar</a></b> Intelligible
semi-automated reasoning --- readable formal proof documents
<li><b><a href="IOA/index.html">Isabelle/IOA</a></b> Verification of
distributed, reactive systems using I/O Automata
-<li> <b>Isabelle/HOOL</b> Object-oriented verification of
+<li><b>Isabelle/HOOL</b> Object-oriented verification of
object-oriented programs
-<li> <b><a href="VerifiCard/">Isabelle/VerifiCard</a></b>
-Tool-assisted Specification and Verification of JavaCard® Programs
+<li><b><a href="VerifiCard/">Isabelle/VerifiCard</a></b> Tool-assisted
+Specification and Verification of JavaCard® Programs
</ul>
--- a/Admin/polyml/makepkg Tue Feb 13 16:05:56 2001 +0100
+++ b/Admin/polyml/makepkg Tue Feb 13 16:31:18 2001 +0100
@@ -4,6 +4,8 @@
SUPER="$(cd "$THIS"; cd ..; echo "$PWD")"
NAME="$(basename "$THIS")"
+[ -h "$NAME" ] && { echo "$NAME is a symlink!"; exit 2; }
+
TAR=tar
type -path gtar >/dev/null && TAR=gtar