--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/isasync Tue Sep 27 15:30:37 2005 +0200
@@ -0,0 +1,131 @@
+#!/usr/bin/env bash
+#
+# $Id$
+#
+# mirror script for Isabelle distribution or website
+
+
+## diagnostics
+
+PRG=`basename "$0"`
+
+usage()
+{
+ echo
+ echo "Usage: $PRG [OPTIONS] DEST"
+ echo
+ echo " Options are:"
+ echo " -h print help message"
+ echo " -n dry run, don't do anything, just report what would happen"
+ echo " -w mirror whole Isabelle website"
+ echo " -d delete files that are not on the server (BEWARE!)"
+ echo
+ exit 1
+}
+
+fail()
+{
+ echo "$1" >&2
+ exit 2
+}
+
+
+## process command line
+
+# options
+
+HELP=""
+ARGS=""
+SRC="isabelle-distribution"
+
+while getopts "hnwd" OPT
+do
+ case "$OPT" in
+ h)
+ HELP=true
+ ;;
+ n)
+ ARGS="$ARGS -n"
+ ;;
+ w)
+ SRC="isabelle-website"
+ ;;
+ d)
+ ARGS="$ARGS --delete"
+ ;;
+ \?)
+ usage
+ ;;
+ esac
+done
+
+shift `expr $OPTIND - 1`
+
+
+# help
+
+if [ -n "$HELP" ]; then
+ cat <<EOF
+
+Mirroring the Isabelle distribution or website
+==============================================
+
+The Munich site maintains an rsync server for the Isabelle
+distribution or website.
+
+The rsync tool is very smart and efficient in mirroring large
+directory hierarchies. See http://rsync.samba.org/ for more
+information. The rsync-isabelle script provides a simple front-end
+for easy access to the Isabelle distribution.
+
+The script can be either run in conservative or clean-sweep mode.
+
+1) Basic mirroring works like this:
+
+ $PRG /foo/bar
+
+where /foo/bar refers to your local copy of the Isabelle distribution
+(the base directory has to exist already). This operation is
+conservative in the sense that files are never deleted, thus garbage
+may accumulate over time as our master copy is changed.
+
+Avoiding garbage in your local copy requires some care. Rsync
+provides a way to delete all additional local files that are absent in
+the master copy. This provides an efficient way to purge large
+directory hierarchies, even unwillingly in case that a wrong
+destination is given!
+
+2a) This will invoke a safe dry-run of clean-sweep mirroring:
+
+ $PRG -dn /foo/bar
+
+where additions and deletions will be printed without any actual
+changes performed so far.
+
+2b) Exact mirroring with actual deletion of garbage may be performed
+like this:
+
+ $PRG -d /foo/bar
+
+
+After gaining some confidence in the workings of rsync-isabelle one
+would usually set up some automatic mirror scheme, e.g. a daily cron
+job run by the 'nobody' user.
+
+Add -w to the option list in order to mirror the whole Isabelle website
+
+EOF
+ exit 0
+fi
+
+
+# arguments
+
+[ $# -ne 1 ] && { echo "Bad arguments: $*"; usage; }
+
+DEST="$1"; shift;
+
+
+## main
+
+exec rsync -va $ARGS "rsync://isabelle.in.tum.de/$SRC/." "$DEST/."
--- a/Admin/mirror-main Tue Sep 27 14:41:41 2005 +0200
+++ b/Admin/mirror-main Tue Sep 27 15:30:37 2005 +0200
@@ -31,4 +31,4 @@
echo "Warning: this script now mirrors the *complete* Isabelle site"
rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync -va --copy-links \
- $USER@sunbroy2.informatik.tu-muenchen.de:/usr/proj/isabelle-repository/www/. $DEST/.
+ $USER@sunbroy2.informatik.tu-muenchen.de:/home/proj/isabelle/website/. $DEST/.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/mirror-website Tue Sep 27 15:30:37 2005 +0200
@@ -0,0 +1,26 @@
+#!/usr/bin/env bash
+#
+# $Id$
+#
+# mirrors the Isabelle website
+
+HOST=$(hostname)
+
+case ${HOST} in
+ sunbroy2)
+ DEST=/home/html/isabelle/html-data
+ ;;
+ atbroy1)
+ DEST=/home/html/isabelle/html-data
+ ;;
+ *.cl.cam.ac.uk)
+ USER=paulson
+ DEST=/anfs/www/html/Research/HVG/Isabelle
+ ;;
+ *)
+ echo "Unknown destination directory for ${HOST}"
+ exit 2
+ ;;
+esac
+
+exec $(dirname $0)/isasync -dw $DEST
--- a/Admin/rsyncd.conf Tue Sep 27 14:41:41 2005 +0200
+++ b/Admin/rsyncd.conf Tue Sep 27 15:30:37 2005 +0200
@@ -1,8 +1,4 @@
-#
# rsync server configuration
-#
-# $Id$
-#
uid = nobody
gid = nobody
@@ -10,7 +6,15 @@
log file = /tmp/rsyncd.log
read only = true
+[isabelle-website]
+ path = /home/proj/isabelle/website
+ comment = Isabelle website
+
+[isabelle-distribution]
+ path = /home/proj/isabelle/website/dist
+ comment = Isabelle distribution
+
+# Sydney legacy link
[isabelle-dist]
- path = /home/html/isabelle/html-data/dist/
- comment = Isabelle distribution area
-
+ path = /home/html/isabelle/html-data/dist/
+ comment = Isabelle distribution area
--- a/Admin/website/build/localconf.at.template.mak Tue Sep 27 14:41:41 2005 +0200
+++ b/Admin/website/build/localconf.at.template.mak Tue Sep 27 15:30:37 2005 +0200
@@ -1,29 +1,29 @@
# isaweb configuration
# $Id$
-# python interpreter (> 2.2)
+# python interpreter (>= 2.3)
PYTHON=python
# GNU find
FIND=find
+# GNU copy
+COPY=cp
+
# HTML tidy (needs not to be set if tidy usage is disabled, see below)
TIDY=tidy
# dirs to copy to build target
-STATICDIRS=css img media misc dist
+STATICDIRS=css img media misc
# build target (attention: ~ will not work!)
-OUTPUTROOT=/home/proj/isabelle/website
+OUTPUTROOT=$(HOME)/isabelle/website_test
# location of isabelle distribution packages
-ISABELLE_DIST=/home/proj/isabelle/dist/Isabelle2004
-
-# location of isabelle library
-ISABELLE_LIBR=/home/proj/isabelle/dist/library-Isabelle2004
+ISABELLE_DIST=/home/proj/isabelle/dist/dist-Isabelle2005
# location of doc content file
-ISABELLE_DOC_CONTENT_FILE=/home/proj/isabelle/Isabelle2004/doc/Contents
+ISABELLE_DOC_CONTENT_FILE=/home/proj/isabelle/dist/dist-Isabelle2005/doc/Contents
# umask for target files
TARGET_UMASK_FILE=664
--- a/Admin/website/build/localconf.sun.template.mak Tue Sep 27 14:41:41 2005 +0200
+++ b/Admin/website/build/localconf.sun.template.mak Tue Sep 27 15:30:37 2005 +0200
@@ -1,29 +1,29 @@
# isaweb configuration
# $Id$
-# python interpreter (> 2.2)
+# python interpreter (>= 2.3)
PYTHON=python2.3
# GNU find
FIND=gfind
+# GNU copy
+COPY=gcp
+
# HTML tidy (needs not to be set if tidy usage is disabled, see below)
TIDY=tidy
# dirs to copy to build target
-STATICDIRS=css img media misc dist
+STATICDIRS=css img media misc
# build target (attention: ~ will not work!)
-OUTPUTROOT=/home/proj/isabelle/website
+OUTPUTROOT=$(HOME)/isabelle/website_test
# location of isabelle distribution packages
-ISABELLE_DIST=/home/proj/isabelle/dist/Isabelle2004
-
-# location of isabelle library
-ISABELLE_LIBR=/home/proj/isabelle/dist/library-Isabelle2004
+ISABELLE_DIST=/home/proj/isabelle/dist/dist-Isabelle2005
# location of doc content file
-ISABELLE_DOC_CONTENT_FILE=/home/proj/isabelle/Isabelle2004/doc/Contents
+ISABELLE_DOC_CONTENT_FILE=/home/proj/isabelle/dist/dist-Isabelle2005/doc/Contents
# umask for target files
TARGET_UMASK_FILE=664
--- a/Admin/website/build/main.mak Tue Sep 27 14:41:41 2005 +0200
+++ b/Admin/website/build/main.mak Tue Sep 27 15:30:37 2005 +0200
@@ -96,7 +96,7 @@
done; \
echo "DEP_ALLSTATIC=$$allstatic" >> $(DEP_FILE); \
echo >> $(DEP_FILE); \
- echo 'DEP_HTML=$$(DEP_ALLSTATIC) $$(DEP_SYMLINKS) include/documentationdist.include.html $(DEP_FILE) $(CONF)' >> $(DEP_FILE); \
+ echo 'DEP_HTML=$$(DEP_ALLSTATIC) include/documentationdist.include.html $(DEP_FILE) $(CONF)' >> $(DEP_FILE); \
echo >> $(DEP_FILE); \
allhtml=''; \
for html in `$(FIND) . -name "*.html" -a ! -name "*.include.html"`; \
--- a/Admin/website/build/project.mak Tue Sep 27 14:41:41 2005 +0200
+++ b/Admin/website/build/project.mak Tue Sep 27 15:30:37 2005 +0200
@@ -1,35 +1,19 @@
# isaweb makefile - project-specific dependencies
# $Id$
-project: site
- chmod -R g-w $(OUTPUTROOT)/dist/packages
+project: $(OUTPUTROOT)/dist site
.PHONY: project
-#~ DEP_SYMLINKS=$(OUTPUTROOT)/dist/packages $(OUTPUTROOT)/library
-
-#~ $(OUTPUTROOT)/dist/packages: $(ISABELLE_DIST)
- #~ mkdir -p $(OUTPUTROOT)/dist
- #~ ln -s $< $@
-
-DEP_SYMLINKS=dist/packages $(OUTPUTROOT)/dist/library
+cleanproject:
+ rm -rf $(OUTPUTROOT)/dist
+.PHONY: cleanproject
-dist/packages: $(ISABELLE_DIST)
- mkdir -p dist
- ln -s $< $@
-
-#~ library: $(ISABELLE_LIBR)
-#~ ln -s $< $@
-
-$(OUTPUTROOT)/dist/library: $(ISABELLE_LIBR)
- mkdir -p $(OUTPUTROOT)/dist
- ln -s $< $@
- chmod $(TARGET_UMASK_DIR) $@
+$(OUTPUTROOT)/dist: $(ISABELLE_DIST)
+ $(COPY) -vRud $< $@
+ chmod -R g-w $@
include/documentationdist.include.html: $(ISABELLE_DOC_CONTENT_FILE)
- perl build/mkcontents.pl -p '//dist/packages/Isabelle/doc/' $< $@
-
-symlinks: $(DEP_SYMLINKS)
-.PHONY: symlinks
+ perl build/mkcontents.pl -p '//dist/Isabelle/doc/' $< $@
include conf/distname.mak
conf/distname.mak:
@@ -38,6 +22,6 @@
echo 'If you have no makedist at hand, allocate a conf/distname.mak file'; \
echo 'yourself, e. g. by:'; \
echo; \
- echo 'echo "DISTNAME=Isabelle2004" > conf/distname.mak'; \
+ echo 'echo "DISTNAME=Isabelle1705" > conf/distname.mak'; \
echo; \
false; \
--- a/Admin/website/documentation.html Tue Sep 27 14:41:41 2005 +0200
+++ b/Admin/website/documentation.html Tue Sep 27 15:30:37 2005 +0200
@@ -23,7 +23,7 @@
width="83" height="125"/>
</a>
<p>For getting started with Isabelle quickly, we recommend the <a href=
- "//dist/packages/Isabelle/doc/tutorial.pdf">Tutorial on
+ "//dist/Isabelle/doc/tutorial.pdf">Tutorial on
Isabelle/HOL</a> (published by Springer Verlag as <a href=
"http://www4.in.tum.de/~nipkow/LNCS2283/">LNCS 2283</a>) and the <a href=
"#course_material">course material</a>.</p>
@@ -51,12 +51,12 @@
<h3>Release notes</h3>
<ul>
- <li><a href="//dist/packages/Isabelle/ANNOUNCE">ANNOUNCE</a></li>
- <li><a href="//dist/packages/Isabelle/README.html">README</a></li>
- <li><a href="//dist/packages/Isabelle/INSTALL">INSTALL</a></li>
- <li><a href="//dist/packages/Isabelle/NEWS">NEWS</a></li>
- <li><a href="//dist/packages/Isabelle/COPYRIGHT">COPYRIGHT</a></li>
- <li><a href="//dist/packages/Isabelle/CONTRIBUTORS">CONTRIBUTORS</a></li>
+ <li><a href="//dist/Isabelle/ANNOUNCE">ANNOUNCE</a></li>
+ <li><a href="//dist/Isabelle/README.html">README</a></li>
+ <li><a href="//dist/Isabelle/INSTALL">INSTALL</a></li>
+ <li><a href="//dist/Isabelle/NEWS">NEWS</a></li>
+ <li><a href="//dist/Isabelle/COPYRIGHT">COPYRIGHT</a></li>
+ <li><a href="//dist/Isabelle/CONTRIBUTORS">CONTRIBUTORS</a></li>
</ul>
<h2 id="course_material">Course Material and Exercises</h2>
--- a/Admin/website/include/documentationdist.include.html Tue Sep 27 14:41:41 2005 +0200
+++ b/Admin/website/include/documentationdist.include.html Tue Sep 27 15:30:37 2005 +0200
@@ -2,26 +2,26 @@
<dummy:wrapper xmlns:dummy="http://nowhere.no">
<h3>Learning Isabelle</h3>
<ul>
- <li><a target='_blank' href='//dist/packages/Isabelle/doc/tutorial.pdf'>Tutorial on Isabelle/HOL</a></li>
- <li><a target='_blank' href='//dist/packages/Isabelle/doc/isar-overview.pdf'>Tutorial on Isar</a></li>
- <li><a target='_blank' href='//dist/packages/Isabelle/doc/locales.pdf'>Tutorial on Locales</a></li>
+ <li><a target='_blank' href='//dist/Isabelle/doc/tutorial.pdf'>Tutorial on Isabelle/HOL</a></li>
+ <li><a target='_blank' href='//dist/Isabelle/doc/isar-overview.pdf'>Tutorial on Isar</a></li>
+ <li><a target='_blank' href='//dist/Isabelle/doc/locales.pdf'>Tutorial on Locales</a></li>
</ul>
<h3>Reference Manuals</h3>
<ul>
- <li><a target='_blank' href='//dist/packages/Isabelle/doc/isar-ref.pdf'>The Isabelle/Isar Reference Manual</a></li>
- <li><a target='_blank' href='//dist/packages/Isabelle/doc/ref.pdf'>The Isabelle Reference Manual</a></li>
- <li><a target='_blank' href='//dist/packages/Isabelle/doc/system.pdf'>The Isabelle System Manual</a></li>
+ <li><a target='_blank' href='//dist/Isabelle/doc/isar-ref.pdf'>The Isabelle/Isar Reference Manual</a></li>
+ <li><a target='_blank' href='//dist/Isabelle/doc/ref.pdf'>The Isabelle Reference Manual</a></li>
+ <li><a target='_blank' href='//dist/Isabelle/doc/system.pdf'>The Isabelle System Manual</a></li>
</ul>
<h3>Logics</h3>
<ul>
- <li><a target='_blank' href='//dist/packages/Isabelle/doc/logics.pdf'>Isabelle's Logics: overview and misc logics</a></li>
- <li><a target='_blank' href='//dist/packages/Isabelle/doc/logics-HOL.pdf'>Isabelle's Logics: HOL</a></li>
- <li><a target='_blank' href='//dist/packages/Isabelle/doc/logics-ZF.pdf'>Isabelle's Logics: FOL and ZF</a></li>
+ <li><a target='_blank' href='//dist/Isabelle/doc/logics.pdf'>Isabelle's Logics: overview and misc logics</a></li>
+ <li><a target='_blank' href='//dist/Isabelle/doc/logics-HOL.pdf'>Isabelle's Logics: HOL</a></li>
+ <li><a target='_blank' href='//dist/Isabelle/doc/logics-ZF.pdf'>Isabelle's Logics: FOL and ZF</a></li>
</ul>
<h3>Specific Topics</h3>
<ul>
- <li><a target='_blank' href='//dist/packages/Isabelle/doc/sugar.pdf'>LaTeX sugar for proof documents</a></li>
- <li><a target='_blank' href='//dist/packages/Isabelle/doc/axclass.pdf'>Tutorial on Axiomatic Type Classes</a></li>
- <li><a target='_blank' href='//dist/packages/Isabelle/doc/ind-defs.pdf'>(Co)Inductive Definitions in ZF</a></li>
+ <li><a target='_blank' href='//dist/Isabelle/doc/sugar.pdf'>LaTeX sugar for proof documents</a></li>
+ <li><a target='_blank' href='//dist/Isabelle/doc/axclass.pdf'>Tutorial on Axiomatic Type Classes</a></li>
+ <li><a target='_blank' href='//dist/Isabelle/doc/ind-defs.pdf'>(Co)Inductive Definitions in ZF</a></li>
</ul>
</dummy:wrapper>
--- a/Admin/website/include/downloadtable.include.html Tue Sep 27 14:41:41 2005 +0200
+++ b/Admin/website/include/downloadtable.include.html Tue Sep 27 15:30:37 2005 +0200
@@ -7,104 +7,104 @@
<td>
Sources and documentation
</td>
- <?downloadCells target="//dist/packages/Isabelle2005.tar.gz" title="Isabelle2005.tar.gz"?>
+ <?downloadCells target="//dist/Isabelle2005.tar.gz" title="Isabelle2005.tar.gz"?>
</tr>
<tr>
<td>
Documentation in PDF
</td>
- <?downloadCells target="//dist/packages/Isabelle2005_pdf.tar.gz" title="Isabelle2005_pdf.tar.gz"?>
+ <?downloadCells target="//dist/Isabelle2005_pdf.tar.gz" title="Isabelle2005_pdf.tar.gz"?>
</tr>
<tr>
<td>
Theory library in PDF and HTML
</td>
- <?downloadCells target="//dist/packages/Isabelle2005_library.tar.gz" title="Isabelle2005_library.tar.gz"?>
+ <?downloadCells target="//dist/Isabelle2005_library.tar.gz" title="Isabelle2005_library.tar.gz"?>
</tr>
<tr><td colspan="3" class="downloadheader">Proof General</td></tr>
<tr>
<td>
Proof General
</td>
- <?downloadCells target="//dist/packages/contrib/ProofGeneral.tar.gz" title="ProofGeneral.tar.gz"?>
+ <?downloadCells target="//dist/contrib/ProofGeneral.tar.gz" title="ProofGeneral.tar.gz"?>
</tr>
<tr><td colspan="3" class="downloadheader">Poly/ML compiler and runtime system</td></tr>
<tr>
<td rowspan="3">
Poly/ML
</td>
- <?downloadCells target="//dist/packages/contrib/polyml_x86-linux.tar.gz" title="polyml_x86-linux.tar.gz"?>
+ <?downloadCells target="//dist/contrib/polyml_x86-linux.tar.gz" title="polyml_x86-linux.tar.gz"?>
</tr>
<tr>
<td style="display: none"></td>
- <?downloadCells target="//dist/packages/contrib/polyml_sparc-solaris.tar.gz" title="polyml_sparc-solaris.tar.gz"?>
+ <?downloadCells target="//dist/contrib/polyml_sparc-solaris.tar.gz" title="polyml_sparc-solaris.tar.gz"?>
</tr>
<tr>
<td style="display: none"></td>
- <?downloadCells target="//dist/packages/contrib/polyml_ppc-darwin.tar.gz" title="polyml_ppc-darwin.tar.gz"?>
+ <?downloadCells target="//dist/contrib/polyml_ppc-darwin.tar.gz" title="polyml_ppc-darwin.tar.gz"?>
</tr>
<tr><td colspan="3" class="downloadheader">Precompiled logics</td></tr>
<tr>
<td rowspan="3">
HOL
</td>
- <?downloadCells target="//dist/packages/HOL_x86-linux.tar.gz" title="HOL_x86-linux.tar.gz"?>
+ <?downloadCells target="//dist/HOL_x86-linux.tar.gz" title="HOL_x86-linux.tar.gz"?>
</tr>
<tr>
<td style="display: none"></td>
- <?downloadCells target="//dist/packages/HOL_sparc-solaris.tar.gz" title="HOL_sparc-solaris.tar.gz"?>
+ <?downloadCells target="//dist/HOL_sparc-solaris.tar.gz" title="HOL_sparc-solaris.tar.gz"?>
</tr>
<tr>
<td style="display: none"></td>
- <?downloadCells target="//dist/packages/HOL_ppc-darwin.tar.gz" title="HOL_ppc-darwin.tar.gz"?>
+ <?downloadCells target="//dist/HOL_ppc-darwin.tar.gz" title="HOL_ppc-darwin.tar.gz"?>
</tr>
<tr>
<td rowspan="3">
HOL-Complex
</td>
- <?downloadCells target="//dist/packages/HOL-Complex_x86-linux.tar.gz" title="HOL-Complex_x86-linux.tar.gz"?>
+ <?downloadCells target="//dist/HOL-Complex_x86-linux.tar.gz" title="HOL-Complex_x86-linux.tar.gz"?>
</tr>
<tr>
<td style="display: none"></td>
- <?downloadCells target="//dist/packages/HOL-Complex_sparc-solaris.tar.gz" title="HOL-Complex_sparc-solaris.tar.gz"?>
+ <?downloadCells target="//dist/HOL-Complex_sparc-solaris.tar.gz" title="HOL-Complex_sparc-solaris.tar.gz"?>
</tr>
<tr>
<td style="display: none"></td>
- <?downloadCells target="//dist/packages/HOL-Complex_ppc-darwin.tar.gz" title="HOL-Complex_ppc-darwin.tar.gz"?>
+ <?downloadCells target="//dist/HOL-Complex_ppc-darwin.tar.gz" title="HOL-Complex_ppc-darwin.tar.gz"?>
</tr>
<tr>
<td rowspan="3">
HOL4
</td>
- <?downloadCells target="//dist/packages/HOL4_x86-linux.tar.gz" title="HOL4_x86-linux.tar.gz"?>
+ <?downloadCells target="//dist/HOL4_x86-linux.tar.gz" title="HOL4_x86-linux.tar.gz"?>
</tr>
<tr>
<td style="display: none"></td>
- <?downloadCells target="//dist/packages/HOL4_sparc-solaris.tar.gz" title="HOL4_sparc-solaris.tar.gz"?>
+ <?downloadCells target="//dist/HOL4_sparc-solaris.tar.gz" title="HOL4_sparc-solaris.tar.gz"?>
</tr>
<tr>
<td style="display: none"></td>
- <?downloadCells target="//dist/packages/HOL4_ppc-darwin.tar.gz" title="HOL4_ppc-darwin.tar.gz"?>
+ <?downloadCells target="//dist/HOL4_ppc-darwin.tar.gz" title="HOL4_ppc-darwin.tar.gz"?>
</tr>
<tr>
<td rowspan="3">
ZF
</td>
- <?downloadCells target="//dist/packages/ZF_x86-linux.tar.gz" title="ZF_x86-linux.tar.gz"?>
+ <?downloadCells target="//dist/ZF_x86-linux.tar.gz" title="ZF_x86-linux.tar.gz"?>
</tr>
<tr>
<td style="display: none"></td>
- <?downloadCells target="//dist/packages/ZF_sparc-solaris.tar.gz" title="ZF_sparc-solaris.tar.gz"?>
+ <?downloadCells target="//dist/ZF_sparc-solaris.tar.gz" title="ZF_sparc-solaris.tar.gz"?>
</tr>
<tr>
<td style="display: none"></td>
- <?downloadCells target="//dist/packages/ZF_ppc-darwin.tar.gz" title="ZF_ppc-darwin.tar.gz"?>
+ <?downloadCells target="//dist/ZF_ppc-darwin.tar.gz" title="ZF_ppc-darwin.tar.gz"?>
</tr>
<tr><td colspan="3" class="downloadheader">HOL4 proof terms</td></tr>
<tr>
<td>
HOL4 proof terms
</td>
- <?downloadCells target="//dist/packages/contrib/HOL4-proofs.tar.gz" title="HOL4-proofs.tar.gz"?>
+ <?downloadCells target="//dist/contrib/HOL4-proofs.tar.gz" title="HOL4-proofs.tar.gz"?>
</tr>
</table>
--- a/Admin/website/index.html Tue Sep 27 14:41:41 2005 +0200
+++ b/Admin/website/index.html Tue Sep 27 15:30:37 2005 +0200
@@ -56,7 +56,7 @@
<li>Major internal reorganizations and performance improvements.</li>
</ul>
-<p><a href="//dist/packages/Isabelle/NEWS">[Cumulative NEWS]</a></p>
+<p><a href="//dist/Isabelle/NEWS">[Cumulative NEWS]</a></p>
<h2>Download</h2>
--- a/Admin/website/installation.html Tue Sep 27 14:41:41 2005 +0200
+++ b/Admin/website/installation.html Tue Sep 27 15:30:37 2005 +0200
@@ -23,7 +23,7 @@
ready-to-use binary packages for Linux/x86, MaxOS X /
Darwin, and Solaris. For other platforms, Isabelle logics
need to be compiled separately (see also <a
- href="//dist/packages/Isabelle/INSTALL">INSTALL</a>).
+ href="//dist/Isabelle/INSTALL">INSTALL</a>).
</p>
<p>
@@ -76,10 +76,10 @@
<li>Unpack the archives to an appropriate location, e. g.
<tt class="shellcmd">/usr/local</tt>:
<ul class="shellcmd">
- <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2005.tar.gz"?></li>
- <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_x86-linux.tar.gz"?></li>
- <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_x86-linux.tar.gz"?></li>
- <li>tar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li>
+ <li>tar -C /usr/local -xzf <?downloadLink target="//dist/Isabelle2005.tar.gz"?></li>
+ <li>tar -C /usr/local -xzf <?downloadLink target="//dist/contrib/polyml_x86-linux.tar.gz"?></li>
+ <li>tar -C /usr/local -xzf <?downloadLink target="//dist/HOL_x86-linux.tar.gz"?></li>
+ <li>tar -C /usr/local -xzf <?downloadLink target="//dist/contrib/ProofGeneral.tar.gz"?></li>
</ul>
</li>
@@ -122,10 +122,10 @@
<li>Unpack the archives to an appropriate location, e. g.
<tt class="shellcmd">/usr/local</tt>:
<ul class="shellcmd">
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2005.tar.gz"?></li>
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li>
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_ppc-darwin.tar.gz"?></li>
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_ppc-darwin.tar.gz"?></li>
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/Isabelle2005.tar.gz"?></li>
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/contrib/ProofGeneral.tar.gz"?></li>
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/contrib/polyml_ppc-darwin.tar.gz"?></li>
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/HOL_ppc-darwin.tar.gz"?></li>
</ul>
</li>
@@ -155,10 +155,10 @@
<li>Unpack the archives to an appropriate location, e. g.
<tt class="shellcmd">/usr/local</tt>:
<ul class="shellcmd">
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/Isabelle2005.tar.gz"?></li>
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/ProofGeneral.tar.gz"?></li>
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/contrib/polyml_sparc-solaris.tar.gz"?></li>
- <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/packages/HOL_sparc-solaris.tar.gz"?></li>
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/Isabelle2005.tar.gz"?></li>
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/contrib/ProofGeneral.tar.gz"?></li>
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/contrib/polyml_sparc-solaris.tar.gz"?></li>
+ <li>gtar -C /usr/local -xzf <?downloadLink target="//dist/HOL_sparc-solaris.tar.gz"?></li>
</ul>
</li>
--- a/Admin/website/overview.html Tue Sep 27 14:41:41 2005 +0200
+++ b/Admin/website/overview.html Tue Sep 27 15:30:37 2005 +0200
@@ -37,7 +37,7 @@
University of Munich, Germany).</p>
<p>Isabelle is distributed <em>freely</em> as Open Source
- Software <!--a href="//dist/packages/Isabelle/COPYRIGHT"-->BSD
+ Software <!--a href="//dist/Isabelle/COPYRIGHT"-->BSD
license<!--/a-->; see the <a
href="installation.html">installation instructions</a>.</p>