tuned;
authorwenzelm
Tue Feb 13 16:31:18 2001 +0100 (2001-02-13)
changeset 11109ce1cefc6c14c
parent 11108 43791f99d71e
child 11110 306beb99e192
tuned;
ANNOUNCE
Admin/page/dist-content/docs.content
Admin/page/dist-content/index.content
Admin/page/dist-content/past.content
Admin/page/main-content/index.content
Admin/page/main-content/logics.content
Admin/page/main-content/munich.content
Admin/polyml/makepkg
     1.1 --- a/ANNOUNCE	Tue Feb 13 16:05:56 2001 +0100
     1.2 +++ b/ANNOUNCE	Tue Feb 13 16:31:18 2001 +0100
     1.3 @@ -12,22 +12,22 @@
     1.4    * Poly/ML 4.0 used by default
     1.5      More robust, less disk space required.
     1.6  
     1.7 -  * Pure/Simplifier (Stefan Berghofer)
     1.8 +  * Simplifier (Stefan Berghofer)
     1.9      Proper implementation as a derived rule, outside the kernel!
    1.10  
    1.11 +  * Improved document preparation (Markus Wenzel)
    1.12 +    Near math-mode, sub/super scripts, more symbols etc.
    1.13 +
    1.14    * Isabelle/Isar (Markus Wenzel)
    1.15      Numerous usability improvements, e.g. support for initial
    1.16      schematic goals, failure prediction of subgoal statements,
    1.17      handling of non-atomic statements in induction.
    1.18  
    1.19 -  * Improved document preparation (Markus Wenzel)
    1.20 -    Near math-mode, sub/super scripts, more symbols etc.
    1.21 -
    1.22    * HOL/Library (Gertrud Bauer, Tobias Nipkow, Lawrence C Paulson,
    1.23        Thomas M Rasmussen, Markus Wenzel)
    1.24      A collection of generic theories to be used together with main HOL.
    1.25  
    1.26 -  * HOL/Real and HOL/Hyperreal (Jacques Fleuriot and Lawrence C Paulson)
    1.27 +  * HOL/Real and HOL/Hyperreal (Jacques Fleuriot, Lawrence C Paulson)
    1.28      General cleanup, more on nonstandard real analysis.
    1.29  
    1.30    * HOL/Unix (Markus Wenzel)
     2.1 --- a/Admin/page/dist-content/docs.content	Tue Feb 13 16:05:56 2001 +0100
     2.2 +++ b/Admin/page/dist-content/docs.content	Tue Feb 13 16:31:18 2001 +0100
     2.3 @@ -13,10 +13,10 @@
     2.4  information about the present release and additional installation
     2.5  instructions.
     2.6  <ul>
     2.7 -<li> <!-- _GP_ href(distname . "/ANNOUNCE", "ANNOUNCE") -->
     2.8 -<li> <!-- _GP_ href(distname . "/README.html", "README") -->
     2.9 -<li> <!-- _GP_ href(distname . "/INSTALL", "INSTALL") -->
    2.10 -<li> <!-- _GP_ href(distname . "/NEWS", "NEWS") -->
    2.11 +<li><!-- _GP_ href(distname . "/ANNOUNCE", "ANNOUNCE") -->
    2.12 +<li><!-- _GP_ href(distname . "/README.html", "README") -->
    2.13 +<li><!-- _GP_ href(distname . "/INSTALL", "INSTALL") -->
    2.14 +<li><!-- _GP_ href(distname . "/NEWS", "NEWS") -->
    2.15  </ul>
    2.16  
    2.17  <p>
     3.1 --- a/Admin/page/dist-content/index.content	Tue Feb 13 16:05:56 2001 +0100
     3.2 +++ b/Admin/page/dist-content/index.content	Tue Feb 13 16:31:18 2001 +0100
     3.3 @@ -11,18 +11,18 @@
     3.4  
     3.5  <ul>	
     3.6  
     3.7 -<li> <a
     3.8 +<li><a
     3.9  href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/packages.html">Cambridge
    3.10  (UK)</a>
    3.11  
    3.12 -<li> <a href="http://isabelle.in.tum.de/dist/packages.html">Munich
    3.13 +<li><a href="http://isabelle.in.tum.de/dist/packages.html">Munich
    3.14  (Germany)</a>
    3.15  	
    3.16 -<li> <a
    3.17 +<li><a
    3.18  href="http://ftp.research.bell-labs.com/dist/smlnj/isabelle/packages.html">New
    3.19  Jersey (USA)</a>
    3.20  
    3.21 -<li> <a
    3.22 +<li><a
    3.23  href="ftp://rodin.stanford.edu/pub/smlnj/isabelle/packages.html">Stanford
    3.24  (USA)</a>
    3.25  
     4.1 --- a/Admin/page/dist-content/past.content	Tue Feb 13 16:05:56 2001 +0100
     4.2 +++ b/Admin/page/dist-content/past.content	Tue Feb 13 16:31:18 2001 +0100
     4.3 @@ -7,12 +7,13 @@
     4.4  Past releases of Isabelle are available from the Cambrige ftp archive:
     4.5  
     4.6  <ul>
     4.7 -<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle99.tar.gz">Isabelle99</a> </li>
     4.8 -<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle98-1.tar.gz">Isabelle98-1</a> </li>
     4.9 -<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle98.tar.gz">Isabelle98</a> </li>
    4.10 -<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-8.tar.gz">Isabelle94-8</a> </li>
    4.11 -<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-7.tar.gz">Isabelle94-7</a> </li>
    4.12 -<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-6.tar.gz">Isabelle94-6</a> </li>
    4.13 -<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94.tar.gz">Isabelle94</a> </li>
    4.14 -<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle93.tar.gz">Isabelle93</a> </li>
    4.15 +<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle99-1.tar.gz">Isabelle99</a></li>
    4.16 +<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle99.tar.gz">Isabelle99</a></li>
    4.17 +<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle98-1.tar.gz">Isabelle98-1</a></li>
    4.18 +<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle98.tar.gz">Isabelle98</a></li>
    4.19 +<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-8.tar.gz">Isabelle94-8</a></li>
    4.20 +<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-7.tar.gz">Isabelle94-7</a></li>
    4.21 +<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-6.tar.gz">Isabelle94-6</a></li>
    4.22 +<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94.tar.gz">Isabelle94</a></li>
    4.23 +<li><a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle93.tar.gz">Isabelle93</a></li>
    4.24  </ul>
     5.1 --- a/Admin/page/main-content/index.content	Tue Feb 13 16:05:56 2001 +0100
     5.2 +++ b/Admin/page/main-content/index.content	Tue Feb 13 16:31:18 2001 +0100
     5.3 @@ -19,11 +19,12 @@
     5.4  
     5.5  <ul>
     5.6  
     5.7 -<li> <a
     5.8 +<li><a
     5.9  href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle
    5.10 -at Cambridge</strong></a> 
    5.11 +at Cambridge</strong></a>
    5.12  
    5.13 -<li> <a href="http://isabelle.in.tum.de/munich.html"><strong>Isabelle at Munich</strong></a>
    5.14 +<li><a href="http://isabelle.in.tum.de/munich.html"><strong>Isabelle
    5.15 +at Munich</strong></a>
    5.16  
    5.17  </ul>
    5.18  
     6.1 --- a/Admin/page/main-content/logics.content	Tue Feb 13 16:05:56 2001 +0100
     6.2 +++ b/Admin/page/main-content/logics.content	Tue Feb 13 16:31:18 2001 +0100
     6.3 @@ -79,16 +79,16 @@
     6.4  
     6.5  <ol>
     6.6  
     6.7 -<li> declare concrete syntax (via mixfix grammar and syntax macros),
     6.8 +<li>declare concrete syntax (via mixfix grammar and syntax macros),
     6.9  
    6.10 -<li> declare abstract syntax (as higher-order constants),
    6.11 +<li>declare abstract syntax (as higher-order constants),
    6.12  
    6.13 -<li> declare inference rules (as meta-logical propositions),
    6.14 +<li>declare inference rules (as meta-logical propositions),
    6.15  
    6.16 -<li> instantiate generic automatic proof tools (simplifier, classical
    6.17 +<li>instantiate generic automatic proof tools (simplifier, classical
    6.18  tableau prover etc.),
    6.19  
    6.20 -<li> manually code special proof procedures (via tacticals or
    6.21 +<li>manually code special proof procedures (via tacticals or
    6.22  hand-written ML).
    6.23  
    6.24  </ol>
     7.1 --- a/Admin/page/main-content/munich.content	Tue Feb 13 16:05:56 2001 +0100
     7.2 +++ b/Admin/page/main-content/munich.content	Tue Feb 13 16:31:18 2001 +0100
     7.3 @@ -24,16 +24,16 @@
     7.4  
     7.5  <ul>
     7.6  
     7.7 -<li> <a href="http://www.in.tum.de/~bauerg/">Gertrud Bauer</a>
     7.8 -<li> <a href="http://www4.in.tum.de/~berghofe/">Stefan Berghofer</a>
     7.9 -<li> <a href="http://www4.in.tum.de/~kleing/">Gerwin Klein</a>
    7.10 -<li> <a href="http://www4.in.tum.de/~narasche/">Wolfgang Naraschewski</a>
    7.11 -<li> <a href="http://www4.in.tum.de/~nipkow/">Tobias Nipkow</a>
    7.12 -<li> <a href="http://www4.in.tum.de/~oheimb/">David von Oheimb</a>
    7.13 -<li> <a href="http://www4.in.tum.de/~prensani/">Leonor Prensa Nieto</a>
    7.14 -<li> <a href="http://www4.in.tum.de/~pusch/">Cornelia Pusch</a>
    7.15 -<li> <a href="http://www4.in.tum.de/~streckem/">Martin Strecker</a>
    7.16 -<li> <a href="http://www4.in.tum.de/~wenzelm/">Markus Wenzel</a>
    7.17 +<li><a href="http://www.in.tum.de/~bauerg/">Gertrud Bauer</a>
    7.18 +<li><a href="http://www4.in.tum.de/~berghofe/">Stefan Berghofer</a>
    7.19 +<li><a href="http://www4.in.tum.de/~kleing/">Gerwin Klein</a>
    7.20 +<li><a href="http://www4.in.tum.de/~narasche/">Wolfgang Naraschewski</a>
    7.21 +<li><a href="http://www4.in.tum.de/~nipkow/">Tobias Nipkow</a>
    7.22 +<li><a href="http://www4.in.tum.de/~oheimb/">David von Oheimb</a>
    7.23 +<li><a href="http://www4.in.tum.de/~prensani/">Leonor Prensa Nieto</a>
    7.24 +<li><a href="http://www4.in.tum.de/~pusch/">Cornelia Pusch</a>
    7.25 +<li><a href="http://www4.in.tum.de/~streckem/">Martin Strecker</a>
    7.26 +<li><a href="http://www4.in.tum.de/~wenzelm/">Markus Wenzel</a>
    7.27  
    7.28  </ul>
    7.29  
    7.30 @@ -42,10 +42,10 @@
    7.31  
    7.32  <ul>
    7.33  
    7.34 -<li> <a href="mailto:buttenbe@in.tum.de">Christian Buttenberg</a> </li>
    7.35 -<li> <a href="http://home.informatik.tu-muenchen.de/~kirsch/">Alexandra Kirsch</a> </li>
    7.36 -<li> <a href="http://www.informatik.tu-muenchen.de/~nanz/">Sebastian Nanz</a> </li>
    7.37 -<li> <a href="http://www.informatik.tu-muenchen.de/~pfeifrot/">Johannes Pfeifroth</a> </li>
    7.38 +<li><a href="mailto:buttenbe@in.tum.de">Christian Buttenberg</a> </li>
    7.39 +<li><a href="http://home.informatik.tu-muenchen.de/~kirsch/">Alexandra Kirsch</a> </li>
    7.40 +<li><a href="http://www.informatik.tu-muenchen.de/~nanz/">Sebastian Nanz</a> </li>
    7.41 +<li><a href="http://www.informatik.tu-muenchen.de/~pfeifrot/">Johannes Pfeifroth</a> </li>
    7.42  
    7.43  </ul>
    7.44  
    7.45 @@ -56,20 +56,20 @@
    7.46  
    7.47  <ul>
    7.48  
    7.49 -<li> <b><a href="Bali/index.html">Isabelle/Bali</a></b> Java and JVM
    7.50 +<li><b><a href="Bali/index.html">Isabelle/Bali</a></b> Java and JVM
    7.51  formalization --- type system, semantics, compilers
    7.52  
    7.53 -<li> <b><a href="Isar/index.html">Isabelle/Isar</a></b> Intelligible
    7.54 +<li><b><a href="Isar/index.html">Isabelle/Isar</a></b> Intelligible
    7.55  semi-automated reasoning --- readable formal proof documents
    7.56  
    7.57  <li><b><a href="IOA/index.html">Isabelle/IOA</a></b> Verification of
    7.58  distributed, reactive systems using I/O Automata
    7.59  
    7.60 -<li> <b>Isabelle/HOOL</b> Object-oriented verification of
    7.61 +<li><b>Isabelle/HOOL</b> Object-oriented verification of
    7.62  object-oriented programs
    7.63  
    7.64 -<li> <b><a href="VerifiCard/">Isabelle/VerifiCard</a></b>
    7.65 -Tool-assisted Specification and Verification of JavaCardŽ Programs
    7.66 +<li><b><a href="VerifiCard/">Isabelle/VerifiCard</a></b> Tool-assisted
    7.67 +Specification and Verification of JavaCardŽ Programs
    7.68  
    7.69  </ul>
    7.70  
     8.1 --- a/Admin/polyml/makepkg	Tue Feb 13 16:05:56 2001 +0100
     8.2 +++ b/Admin/polyml/makepkg	Tue Feb 13 16:31:18 2001 +0100
     8.3 @@ -4,6 +4,8 @@
     8.4  SUPER="$(cd "$THIS"; cd ..; echo "$PWD")"
     8.5  NAME="$(basename "$THIS")"
     8.6  
     8.7 +[ -h "$NAME" ] && { echo "$NAME is a symlink!"; exit 2; }
     8.8 +
     8.9  TAR=tar
    8.10  type -path gtar >/dev/null && TAR=gtar
    8.11