--- a/Admin/page/Contents Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,18 +0,0 @@
-Learning Isabelle
- tutorial Tutorial on Isabelle/HOL
- isar-overview Tutorial on Isar
- locales Tutorial on Locales
-
-Reference Manuals
- isar-ref The Isabelle/Isar Reference Manual
- ref The Isabelle Reference Manual
- system The Isabelle System Manual
-
-Logics
- logics Isabelle's Logics: overview and misc logics
- logics-HOL Isabelle's Logics: HOL
- logics-ZF Isabelle's Logics: FOL and ZF
-
-Specific Topics
- axclass Tutorial on Axiomatic Type Classes
- ind-defs (Co)Inductive Definitions in ZF
--- a/Admin/page/DISTNAME Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,1 +0,0 @@
-Isabelle2004
--- a/Admin/page/HOWTO Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,63 +0,0 @@
-This file describes how to change and regenerate the Isabelle web pages.
-See the bottom of the file for a short overview of the setup.
-
-== Changes to main ==
-
-To make changes to the content of the main pages:
-
- * Edit or add the appropriate Admin/page/main-content/*.content files
- * Run "make clean main" in Admin/page/
- * Check generated html in Admin/page/main/
- * Check changes in main-content into cvs
- * Run "make pub-main" to publish to the Munich web site
- * Run "mirror-main" in Cambridge to synchronize
-
-
-== Changes to dist ==
-
-These should be rare and are a bit more involved at the moment. The
-principle is the same as for the main pages, but the script needs
-access to the distribution files to calculate sizes etc:
-
- * Edit or add the appropriate Admin/page/dist-content/*.content files
- * Make sure the Isabelle package files are available in directory Admin/page.
- On sunbroy2, the following does the trick (in directory Admin/page):
-
- ln -s /home/html/isabelle/html-data/dist/contrib
- for f in /home/html/isabelle/html-data/dist/*.tar.gz; do ln -s $f; done
-
- * Run "make clean dist" in Admin/page/
- * Check generated html in Admin/page/dist/
- * Check changes in dist-content into cvs
- * Run "make pub-dist" to publish to the Munich web site
- (will only copy *.html files, will not update other distribution files)
- * Run "mirror-dist" in Cambridge and notify other mirrors to synchronize
-
-
-== Overview ==
-
-The pages are separated into two sets:
- * main, for the main home page in Munich and Cambridge, and
- * dist, for the current Isabelle distribution more widely mirrored.
-
-Both are generated by a script (genpage) that takes *.content files and
-puts them into a common template.
-
-This is supposed to achieve the following:
- * separation of layout and content
- * automatic consistency between contents of distribution and web
- page, including name of the distribution, file sizes of download
- packages, and documentation generated from isabelle/Doc
-
-For this the web page generation script needs access to the following
-support files:
-
-Admin/page/DISTNAME (name of the distribution, e.g. Isabelle2004)
-Admin/page/Contents (same as Distribution/doc/Contents at the time
- of the Isabelle release)
-
-Both files are set to the right values automatically by makedist when
-the Isabelle distribution is generated and maintained manually in
-between releases by the release manager in Admin/page in CVS. (In
-between releases Admin/page/Contents can be different from
-Distribution/doc/Contents)
--- a/Admin/page/Makefile Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,99 +0,0 @@
-# -- makefile for Isabelle web pages (dist and main)
-# -- $Id$
-
-# --- force shell
-SHELL=bash
-
-# --- check parameters
-ifeq ($(tidy),)
- TIDYCMD=:
-else
- TIDYCMD=tidy -q -i -asxhtml --doctype auto --indent-spaces 2 --wrap 80 \
- --logical-emphasis yes --gnu-emacs yes --write-back yes
-endif
-
-# --- external tools
-
-GENPAGE = ./bin/genpage
-MKCONTENT = ./bin/mkcontents
-
-# ---
-# --- genpage stuff
-
-# --- directories for main isabelle pages
-
-MAIN_CONTENT = main-content
-MAIN_LAYOUT = main-layout
-MAIN_TARGET = main
-
-# --- directories for isabelle distribution pages
-
-DIST_CONTENT = dist-content
-DIST_LAYOUT = dist-layout
-DIST_TARGET = dist
-
-# --- name of genpage template file
-TEMPLATE_NAME = template.html
-
-# ---
-# --- doc content generation
-
-# --- location of the Contents file of the Isabelle documentation
-DOC_CONTENT_FILE = Contents
-
-# --- target include files with documentation links
-DOC_CONTENTS_MAIN = docu-contents.main
-DOC_CONTENTS_DIST = docu-contents.dist
-
-# --- target directories for publishing to web site
-MAIN_PUB_MIRROR_SRC=sunbroy2.informatik.tu-muenchen.de:/home/proj/isabelle-repository/www/
-MAIN_PUB_DEST=sunbroy2.informatik.tu-muenchen.de:/home/html/isabelle/html-data/
-DIST_PUB_DEST=sunbroy2.informatik.tu-muenchen.de:/home/html/isabelle/html-data/dist/
-
-# ---
-# --- begin rules
-
-all: clean main dist install weblint
-
-main:
- @$(MKCONTENT) -p dist/`cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_MAIN)
- @env DISTNAME=`cat DISTNAME` \
- $(GENPAGE) -t $(MAIN_LAYOUT)/$(TEMPLATE_NAME) -c $(MAIN_CONTENT) -o $(MAIN_TARGET)
- -@cd $(MAIN_TARGET); \
- for html in *.html; \
- do $(TIDYCMD) $$html; \
- done
-
-pub-main: main
- @echo "Publishing main pages (*.html only)."
- scp main/*.html $(MAIN_PUB_MIRROR_SRC)
- scp main/*.html $(MAIN_PUB_DEST)
-
-dist:
- @$(MKCONTENT) -p `cat DISTNAME`/doc/ $(DOC_CONTENT_FILE) $(DOC_CONTENTS_DIST)
- @env DISTNAME=`cat DISTNAME` \
- $(GENPAGE) -t $(DIST_LAYOUT)/$(TEMPLATE_NAME) -c $(DIST_CONTENT) -o $(DIST_TARGET)
- -@cd $(MAIN_TARGET); \
- for html in *.html; \
- do $(TIDYCMD) $$html; \
- done
-
-pub-dist: dist
- @echo "Publishing dist pages (*.html only)."
- scp dist/*.html $(DIST_PUB_DEST)
-
-install: main dist
- @cp -R dist/. ..
- @mkdir -p ../../main-`cat DISTNAME`/.
- @cp -R main/. ../../main-`cat DISTNAME`/.
-
-weblint:
- -weblint -x netscape -d extension-attribute -e img-size $(MAIN_TARGET)
- -weblint -x netscape -d extension-attribute -e img-size $(DIST_TARGET)
-
-clean:
- @rm -rf $(MAIN_TARGET)
- @rm -rf $(DIST_TARGET)
- @rm -rf $(DOC_CONTENTS_MAIN)
- @rm -rf $(DOC_CONTENTS_DIST)
- @find . -name "*~" -type f -print | xargs rm -f
--- a/Admin/page/bin/genpage Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,420 +0,0 @@
-#!/usr/bin/perl -w
-
-# Genpage - Webpage Generator.
-#
-# Copyright (C) Joe Vaughan <joev@freddyfrog.com> 1998-1999
-# Some portions Copyright (C) Ronan Waide <waider@waider.ie> 1999
-# Some portions Copyright (C) Rocco Caputo <troc@netrus.net> 1999
-#
-# This program is free software; you can redistribute it and/or modify
-# it under the terms of the GNU General Public License as published by
-# the Free Software Foundation; either version 2 of the License, or
-# (at your option) any later version.
-#
-# This program is distributed in the hope that it will be useful,
-# but WITHOUT ANY WARRANTY; without even the implied warranty of
-# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
-# GNU General Public License for more details.
-#
-# You should have received a copy of the GNU General Public License
-# along with this program; if not, write to the Free Software
-# Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
-
-$|=1;
-
-$version = "1.0b3";
-
-# following fix for Mac Perl submitted by Dair Grant <dair@webthing.net>
-# I shoulda thought of this, but I don't have a mac :) Thanks Dair.
-#
-# dair, construct a path procedurally
-sub build_path
-{
-
- # Retrieve our parameters
- #
- my $thePath = $_[0];
- my $theItem = $_[1];
-
-
-
- # If we're running on a Mac, munge the path/item/separator
- #
- if ($^O eq "MacOS")
- {
- $thePath =~ s/:$//; # Strip off trailing ':'
- $theItem =~ s/^:$//; # Drop theItem == ':'
- $pathDiv = ":"; # Use Mac separator
- }
- else
- {
- $pathDiv = "/"; # Use Unix separator
- }
-
-
-
- # Return the path to the item
- #
- return($thePath . $pathDiv . $theItem);
-}
-
-
-
-# Some handy variables.
-$numfiles = 0;
-$numcontentfiles = 0;
-$numignoredfiles = 0;
-$numskippedfiles = 0;
-$numcpfiles = 0;
-$numdirfiles =0;
-
-use Getopt::Std;
-use File::Find;
-use File::Copy 'cp';
-
-# Current Working Dir.
-$pwd = `pwd`;
-chomp ($pwd);
-
-getopts('dt:c:o:fqhi:') || die "Invalid args, use $0 -h for help\n";
-
-# $opt_d is debug flag
-# $opt_t is template file. If not set, use standard template.
-# $opt_c is content directory. If not set, use standard content dir.
-# $opt_o is output dir, if not set, use standard output dir.
-# $opt_q sets quiet mode (no stdout output)
-# $opt_f sets a force flag - force generation even if output file is present
-# and newer.
-# $opt_h runs usage and exits
-
-# dair, build paths procedurally
-$opt_t ||= build_path("", "layout") . build_path("", "template.html");
-$opt_c ||= build_path("", "content");
-$opt_o ||= build_path("", "www");
-$opt_f ||= 0;
-$opt_d ||= 0;
-$opt_q ||= 0;
-$opt_h ||= 0;
-$opt_i ||= 'CVS|.*,v$';
-
-# dair, build paths procedurally
-$opt_t = build_path($pwd, $opt_t);
-$opt_c = build_path($pwd, $opt_c);
-$opt_o = build_path($pwd, $opt_o);
-
-
-if ($opt_h) { &usage; }
-
-if (!$opt_q) {
- print "Genpage, version $version starting run...\n";
-}
-
-if ($opt_d) { print "pwd = $pwd\n"; }
-
-#Swallow template file whole...
-open( TEMPLATE, "<$opt_t" ) || die "Can\'t open template file $opt_t: $!\n";
-{
-local $/;
-undef $/;
-$template = <TEMPLATE>;
-close( TEMPLATE );
-}
-if (!$opt_q) {print "Using template file: $opt_t\n";}
-
-# Go through files in content dir and if it's a content file then
-# process it otherwise, copy it (and it's dir structure) to the output dir.
-
-# if the output dir doesn't exist, create it.
-if (! -d $opt_o)
-{
- mkdir $opt_o, 0755;
- if (!$opt_q)
- {
- print "Creating output directory: $opt_o\n";
- }
-}
-
-if (!$opt_q)
- {
- print "Processing files:\n";
- }
-
-if (! -d $opt_c) { die "Can\'t open content dir\n" }
-
-find( \&process_file, $opt_c );
-
-if (!$opt_q)
- {
- #numfiles reports one too many...
- $numfiles--;
- print "\nFinished.\n\n";
- print "Run Summary.\n===========\n";
- print "$numfiles total files and directories processed.\n";
- print "$numcontentfiles content files parsed.\n";
- print "$numskippedfiles content files skipped.\n";
- print "$numcpfiles files copied.\n";
- print "$numdirfiles directories created\n";
- print "$numignoredfiles files or directories ignored.\n";
- }
-
-exit;
-
-##############################################################################
-# Process_file the current file.
-##############################################################################
-sub process_file
- {
- if (!$opt_q)
- {
- print ".";
- }
-
- $numfiles++;
- my $filename = $_;
- my $dir = $File::Find::dir;
- (undef,$reldir) = split( $opt_c, $dir);
- if (!defined ($reldir) ) { $reldir = ""; }
-
- # dair, build paths procedurally
- $outdir = build_path($opt_o, $reldir);
- $outfile = build_path($outdir, $filename);
- $infile = build_path($dir, $filename);
-
- # Ignore CVS stuff, ./ etc.
- if ($infile =~ /$opt_i/) {
- $numignoredfiles++;
- return;
- }
-
- # Find returns ./ in each directory... avoid.
-
- if ($infile =~ /\/.$/) {
- return;
- }
-
- # Ok, If the file is a dir, we create it (if necessary)
- # if it's a content file, we parse it, otherwise, we
- # copy it to the appropriate location.
-
- if ( -d $infile ) {
- if ($opt_d) { print "Making dir $outfile\n"; };
- mkdir $outfile, 0755 unless -d $outfile;
- $numdirfiles++;
- return;
- }
-
- if ($filename =~ /^(.*)\.content$/)
- {
-
- # dair, build paths procedurally
- $outfile = build_path($outdir, "$1.html");
-
- if ($opt_d) {print "Parsing: $infile\n Outputing to: $outfile\n";};
- process_content($infile,$outfile);
- }
- else
- {
- if ($opt_d) { print "Copying: $infile => $outfile\n"; };
- cp($infile,$outfile);
- $numcpfiles++;
- }
- $_ = $filename; # because we broke it...
- }
-
-##############################################################################
-# Process the tags in the template, substituting in the content file
-# components and other things like inline function definitions and
-# "include" directives
-##############################################################################
-
-sub process_content
- {
-
- $inputfile = shift;
- $outputfile = shift;
- my @content = "";
-
- $temp = $template;
-
- if ($opt_d) { print "processing $inputfile to $outputfile\n";}
-
-# Make-like check for last modification times to see if it's necessary
-# to re-gen this page.
-
- if ( -f $outputfile)
- {
-
- if (!$opt_f && ( -M $outputfile < -M $inputfile))
- {
- $numskippedfiles++;
- if ($opt_d) {
- print "skipping $inputfile because $outputfile is newer\n";
- }
- return;
- }
- }
- # Read content file
- open( CONTENT, "<$inputfile" ) || die $!;
- @content = <CONTENT>;
- close( CONTENT );
-
- $numcontentfiles++;
-
- undef %page;
- undef $tag;
- foreach $line ( @content )
- {
- if ( $line =~ /^\s*\%(.+)\%/ )
- {
- $tag = $1;
- next;
- }
- next if !defined( $tag );
-
- $line .= "\n" if $line !~ /\n$/;
-
- if ( defined( $page{ $tag } ))
- {
- $page{ $tag } .= $line;
- }
- else
- {
- $page{ $tag } = $line;
- }
- }
-
- open( HTML, ">$outputfile" ) || die $1;
-
- while ($temp =~ /^(.*?)<!--\s*_GP_\s*(.*?)\s*-->(.*)$/s)
- {
- local $replacement = "";
- my ($left, $middle, $right) = ($1, $2, $3);
- if (!defined($replacement = eval ($middle)))
- {
- $replacement = "";
- }
-
- if ($@) {
- $middle =~ s/\s+/ /g;
- print STDERR "error evaluating { $middle }: $@\n";
- }
- else {
- if ($opt_d) {
- print "evaluation output: $replacement\n";
- }
- }
-
- $temp = $left . $replacement . $right;
- }
- print HTML $temp;
- close( HTML );
- }
-
-
-sub include
- {
- my ($file) = shift;
- my ($section) = shift;
-
- if ($opt_d) {
- print "include: file = $file\n";
- }
- if (!open( INCLUDE, "<$file" )) {
- return "<!-- include: file not found: $file -->";
- }
-
- if (defined($section)) {
- undef %incpage;
- undef $inctag;
-
- @content = <INCLUDE>;
- close (INCLUDE);
-
- foreach $line ( @content )
- {
- if ( $line =~ /^\s*\%(.+)\%/ )
- {
- $inctag = $1;
- next;
- }
- next if !defined( $inctag );
- $line .= "\n" if $line !~ /\n$/;
-
- if ( defined( $incpage{ $inctag } ))
- {
- $incpage{ $inctag } .= $line;
- }
- else
- {
- $incpage{ $inctag } = $line;
- }
- }
- if (defined( $incpage{$section}) ) {
- $inline = $incpage{$section};
- }
- else {
- $inline = "<!-- include: no such section - $section - in $file -->";
- }
- }
- else
- {
- local $/;
- undef $/;
- $inline = <INCLUDE>;
- close( INCLUDE );
- }
- return "$inline";
- }
-
-sub content
- {
- my $tag = shift;
-
- if ($opt_d) { print "content: tag = $tag\n"; }
- if (defined( $page{ $tag } ))
- {
- $output = $page { $tag };
- if ($opt_d) { print "content: output = $output\n"; }
- return "$output";
- }
- else
- {
- return "<!-- content: undefined tag: $tag -->";
- }
- }
-
-sub version
- {
- return ( "<a href=\"http://www.mnemonic.org/genpage/\">Genpage</a> - Version: $version" );
- }
-
-sub usage
- {
- print <<EOT;
-usage: genpage [-dqfh] [-c <content dir>] [-o <output dir>]
- [-t <template file>] [ -i <ignore regexp> ]
-
-
- -d debug mode. Turn on debugging (very verbose!)
- -q quiet mode. Don't print anything while running.
- -f force mode. Force the parsing of content files.
- -h help. Print this help text.
- -c <content dir> The directory where your content tree exists.
- Defaults to ./content.
- -o <output dir> The directory to put the output website.
- Defaults to ./www
- -t <template file> The template to use to generate the site.
- Defaults to ./layout/template.html
- -i <ignore regexp> Regular expression telling genpage to ignore certain
- files or directories. defaults to "CVS|.*,v$"
-
- Genpage $version Copyright (C) Joe Vaughan <joev\@mnemonic.org> 1999
- This program is released under the terms of the GNU Public License
- Please read the accompanying COPYING file for details.
-
- For detailed instructions on how to use Genpage, please consult the
- accompanying documentation. If you have questions, comments or
- suggestions for Genpage please contact the author.
-EOT
-exit;
-}
--- a/Admin/page/bin/mkcontents Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,64 +0,0 @@
-#!/usr/bin/perl
-
-# mkcontents.pl
-#
-# $Id$
-#
-# simple script to create a html version of the Contents file in the
-# Isabelle documentation directory.
-#
-# Nov/14/1999 Version 1.0 - Gerwin Klein <kleing@in.tum.de>
-#
-# command line:
-# mkcontent [-p <url-path-prefix>] <Content-file> <output-file>
-#
-
-
-use Getopt::Long ;
-
-$opt_p="";
-$result = GetOptions ("p=s");
-
-$path=$opt_p;
-
-$infile = $ARGV[0];
-$outfile = $ARGV[1];
-
-$listHeader = "<ul>\n";
-$lineHeader = " <li>";
-$lineEnd = "</li>\n";
-$listFooter = "</ul>\n";
-
-$topicStart = "<h2>";
-$topicEnd = "</h2>\n";
-
-open(IN, "<$infile") || die "cannot read input file <$infile>";
-open(OUT, ">$outfile") || die "cannot write output file <$outfile>";
-
-$first = 1;
-while (<IN>) {
- if (/^([^ \t].*)\n/) {
- if ($first == 1) {
- $first = 0;
- }
- else {
- print OUT $listFooter;
- }
- print OUT $topicStart;
- print OUT $1;
- print OUT $topicEnd;
- print OUT $listHeader;
- }
- elsif (/^[ \t]+([^ \t]+)[ \t]+(.+)\n/) {
- print OUT $lineHeader;
- print OUT "<a href=\"$path$1.pdf\">$2</a>";
- print OUT $lineEnd;
- }
-}
-
-print OUT $listFooter;
-
-close(OUT);
-close(IN);
-
-exit(0);
--- a/Admin/page/common/functions.pl Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,160 +0,0 @@
-<!-- _GP_
-# undef all the functions we're defining. This stops lots of
-# complaining about re-defining the sub for each content file that's
-# processed.
-
- if (defined(&me)) { undef &me; }
- if (defined(&distname)) { undef &distname; }
- if (defined(&href)) { undef &href; }
- if (defined(&twodig)) { undef &twodig; }
- if (defined(&when)) { undef &when; }
- if (defined(&size)) { undef &size; }
- if (defined(&page)) { undef &page; }
- if (defined(&empty_line)) { undef &empty_line; }
- if (defined(&setnavcolor)) { undef &setnavcolor; }
- if (defined(&twodig)) { undef &twodig; }
- if (defined(&setdowncolor)) { undef &setdowncolor; }
- if (defined(&downloadhead)) { undef &downloadhead; }
- if (defined(&download)) { undef &download; }
-
- -->
-
-<!-- _GP_
-
- sub distname {
- return $ENV{"DISTNAME"};
- }
-
- sub href {
- return "<a href=\"" . $_[0] . "\">" . $_[1] . "</a>";
- }
-
- sub twodig {
- if ($_[0] < 10) {
- return "0$_[0]";
- }
- return "$_[0]";
- }
-
-# ($sec,$min,$hour,$mday,$mon,$year,$wday,$yday,$isdst) = gmtime(time);
- sub when {
- my @s = stat $inputfile;
- my @t = gmtime($s[9]);
- my $year = $t[5]+1900;
- my $month = twodig($t[4]+1);
- my $day = twodig($t[3]);
- return "$year-$month-$day";
-# my $hour = twodig($t[2]);
-# my $min = twodig($t[1]);
-# return "$month/$day/$year $hour:$min UTC";
- }
-
- sub setnavcolor {
- $navcolor = $_[0];
- return "";
- }
-
- # page(name, file)
- sub page {
- my $retval = "";
-
- if ("$_[1].html" eq substr($outputfile,rindex($outputfile,"/")+1)) {
- $retval = <<EOF;
- <table width="188" border="0" cellspacing="0" cellpadding="5">
- <tr>
- <td width="8" bgcolor="$navcolor"> </td>
- <td width="160" align="center" bgcolor="$navcolor">
- <b><font face="Arial,Helvetica"><A HREF="$_[1].html" target="_top">$_[0]</A></font></b>
- </td>
- <td width="8" bgcolor="$navcolor"> </td>
- </tr>
- </table>
-EOF
- }
- else {
- $retval = <<EOF;
- <table width="188" border="0" cellspacing="0" cellpadding="5">
- <tr>
- <td width="8"> </td>
- <td width="160" align=center bgcolor="$navcolor">
- <b><font face="Arial,Helvetica"><A HREF="$_[1].html" target="_top">$_[0]</A></font></b>
- </td>
- <td width="8"> </td>
- </tr>
- </table>
-EOF
- }
- return $retval;
- }
-
- # empty_line(numcols)
- sub empty_line {
- my $retval = <<EOF;
- <div style="height: 13px"></div>
-EOF
- return $retval;
- }
-
- sub size {
- my $filename = $_[0];
-
- my @s = stat $filename;
- my $size = defined $s[7] ? $s[7]/1024 : 0;
-
- return sprintf("%d", $size);
- }
-
- sub setdowncolor {
- $downcolor = $_[0];
- return "";
- }
-
- sub downloadhead {
- my $text = $_[0];
-
- return <<EOF;
- <tr><td colspan=3><strong>$text</strong></td></tr>
-EOF
- }
-
- sub download {
- my $rowspan = $_[0];
- my $descr = $_[1];
- my $url = $_[2];
- my $prefix = $_[3];
-
- my $size = size("$prefix/$url");
- $size = "$size K";
-
- my $filename = $path;
-
- if ($url =~ /([^\/]*\/)*([^\/]+)/) {
- $filename = $2;
- }
-
- my $td = "nowrap bgcolor=$downcolor";
-
- my $descr_text = "";
- if ($descr ne "") {
- $descr_text = <<EOF;
- <td rowspan=$rowspan align="left" $td>
- $descr
- </td>
-EOF
- }
-
- my $retval = <<EOF;
- <tr>$descr_text
- <td align="left" $td>
- <A HREF="$url">$filename</A>
- </td>
- <td align="right" $td>
- $size
- </td>
- </tr>
-EOF
-
- return $retval;
- }
-
- -->
--- a/Admin/page/dist-content/docs.content Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-%title%
-Isabelle Documentation
-
-%body%
-
-<!-- _GP_ distname --> documentation is included here as browsable PDF
-for convenience. These documents are also part of the standard
-Isabelle distribution. For getting started with Isabelle quickly, we
-recommend the <a href="<!-- _GP_ distname -->/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="http://isabelle.in.tum.de/coursematerial/">course material</a>
-page. See the
-<a href="http://isabelle.in.tum.de/faq.html">FAQ</a> for answers to frequent problems.
-
-<!-- _GP_ include("$pwd/docu-contents.dist") -->
-
-The Isabelle distribution also includes a few text files with further
-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") -->
-</ul>
-
-<p>
-
-Use the mailing list <a
-href="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a>
-and its <a href="http://www.cl.cam.ac.uk/users/lcp/archive/">archive</a> to
-discuss problems and results. To subscribe, <a href="mailto:lcp@cl.cam.ac.uk?subject=subscribe&body=Please%20add%20me%20to%20the%20Isabelle%20mailing%20list">contact Larry Paulson</a>.
-
Binary file Admin/page/dist-content/favicon.ico has changed
--- a/Admin/page/dist-content/index.content Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,34 +0,0 @@
-
-<!-- $Id$ -->
-
-%title%
-Isabelle Distribution Area
-
-%body%
-<p>
-
-<h2>Stable Release, mirror sites (in alphabetical order)</h2>
-
-<ul>
-
-<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
-(Germany)</a>
-
-<li><a href="http://mirror.cse.unsw.edu.au/pub/isabelle/packages.html">Sydney (Australia)</a>
-
-</ul>
-
-
-
-
-<p>
-
-<h2>Development Snapshot</h2>
-
-For the curious we provide a nightly generated CVS <a
-href="http://isabelle.in.tum.de/devel/">development snapshot</a> of
-Isabelle.
Binary file Admin/page/dist-content/isabelle_macos_screenshot.jpg has changed
--- a/Admin/page/dist-content/notes_macos_darwin.content Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,100 +0,0 @@
-%title%
-Isabelle under Mac OS X
-
-%body%
-
-<p><a href="http://www.apple.com/macosx/">Mac OS X</a> is the current version
-of the Macintosh operating system, installed on all new <a href=
-"http://www.apple.com/">Apple</a> computers. Because it is based on Unix, it
-can run <a href=
-"http://www.cl.cam.ac.uk/Research/HVG/Isabelle/">Isabelle</a>. The new
-<a href="http://www.apple.com/powermac/">Power Mac G5</a> is an excellent
-Isabelle machine. Here is a <a href="isabelle_macos_screenshot.jpg">screenshot</a>
-showing Proof General running in GNU Emacs.</p>
-
-<p>This page gives advice on building Isabelle for Mac OS X. It assumes that
-you are familiar with both Mac OS X and Unix. You must have installed the Mac
-OS X developer tools.</p>
-
-<ol>
-<li>Download Isabelle to a suitable directory, as described on the
-<a href="packages.html">download page</a>. Be sure to get the following files
-
-<ul>
-<li><tt><!-- _GP_ href(distname . ".tar.gz", distname . ".tar.gz") --></tt></li>
-<li><tt><!-- _GP_ href("contrib/ProofGeneral.tar.gz", "ProofGeneral.tar.gz") --></tt></li>
-<li><tt><!-- _GP_ href("contrib/polyml_base.tar.gz", "polyml_base.tar.gz") --></tt></li>
-<li><tt><!-- _GP_ href("contrib/polyml_ppc-darwin.tar.gz", "polyml_ppc-darwin.tar.gz") --></tt></li>
-<li><tt><!-- _GP_ href("HOL_ppc-darwin.tar.gz", "HOL_ppc-darwin.tar.gz") --></tt></li>
-</ul>
-</li>
-
-<li>You may have to install the bash shell. Versions of Mac OS X prior to
-10.2.2 did not provide it. If /bin/bash does not exist, you can install it
-using the package manager <a href=
-"http://fink.sourceforge.net/">Fink</a>.</li>
-
-<li>At this point, you should be able to run Isabelle with the command line
-interface. You can also build Isabelle from the Unix command line,
-following the instructions for "Compiling Logics" in file
-<tt>Isabelle/INSTALL.</tt></li>
-
-<li>You should also be able to launch <a
-href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a> by typing
-"<tt>Isabelle</tt>" at the Unix command line. This will invoke the
-Apple-supplied version of Emacs in a terminal window, providing a
-primitive environment. Somewhat better is to run Proof General from
-within a version of Emacs ported as a native Mac OS X application,
-such as <a href=
-"http://home.att.ne.jp/alpha/z123/emacs-mac-e.html">MacEmacs JP</a> or
-<a href="http://mindlube.com/products/emacs/">mindlube's</a> or <a
-href= "http://www.cs.man.ac.uk/%7efranconi/mac-emacs/">Enhanced Carbon
-Emacs</a>. Visiting a theory file from Emacs will automatically
-launch Proof General provided <tt>isabelle</tt> is on the search
-path. None of these options support the X-Symbol package,
-unfortunately.</li> </ol>
-
-<p>In order to get the full benefit of Proof General, you must install the X
-Window System (X11) and <a href="http://www.xemacs.org/">XEmacs</a> or
-<a href="http://www.gnu.org/software/emacs/emacs.html">GNU Emacs</a>.</p>
-
-<ul>
-<li><a href="http://www.apple.com/macosx/x11/">Apple's version</a> of X11
-is included with the Panther (MacOS 10.3) installation discs, though it is
-not installed by default. The Command key serves as Meta, but it is
-reserved for standard Apple shortcuts such as C, V and X, so you must use
-Esc-C, Esc-V and Esc-X in Emacs or else deselect "Enable key equivalents"
-in the X11 preferences.</li>
-
-<li>Some people prefer the <a href=
-"http://www.osxgnu.org/software/Xwin/WindowManagers/OroborOSX/">OroborOSX</a>
-window manager. It must be used in conjunction with <a href=
-"http://xfree86.org/">XFree86</a>, which is easy to install if you use the
-installer provided by the <a href=
-"http://sourceforge.net/projects/xonx/">XonX</a> project.</li>
-</ul>
-
-<p>The easiest way to install XEmacs or GNU Emacs is via the package manager
-<a href="http://fink.sourceforge.net/">Fink</a>. Install the Fink package
-<tt>xemacs-sumo-pkg</tt> to get the XEmacs libraries that Proof General needs
-to run. To install GNU Emacs, install the package <tt>emacs21</tt>. Fink can
-compile from sources, but this takes hours, so it is better to request binary
-installations.</p>
-
-<p>To use <a href="http://www.gnu.org/software/emacs/emacs.html">GNU
-Emacs</a> instead of <a href="http://www.xemacs.org/">XEmacs</a>, you must
-recompile Proof General and X-Symbol following the instructions <a href=
-"http://proofgeneral.inf.ed.ac.uk/FAQ">here</a>. Note that Proof General
-incorporates its own copy of X-Symbol.</p>
-
-<ol>
-<li>Install X11 or OroborOSX.</li>
-
-<li>Install XEmacs (and its libraries), or install GNU Emacs and recompile
-Proof General.</li>
-
-<li>You may want to install this drag-and-drop <a href=
-"IsabelleDroplet.dmg">Isabelle launcher</a>. It is a simple hack that
-invokes xemacs on any files dropped on it.</li>
-</ol>
-
--- a/Admin/page/dist-content/notes_win_cygwin.content Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,266 +0,0 @@
-%title%
-Isabelle on Windows
-
-%body%
-
-<h2>Preconditions and restrictions</h2>
-
-<p>Please notice before you go ahead:
-<ul>
- <li>The ML system these notes apply to is
- <a href="http://www.smlnj.org/">Standard ML of New Jersey</a>;
- it is <em>not</em> known yet how to get Isabelle run completely with
- <a href="www.polyml.org/">Poly/ML</a>. See <a href="#polyml">a note
- on Poly/ML</a> down this page.</li>
- <li>It is assumed you have some experience with an Unix operating
- system (e.g. what a shell is for and how to use it).</li>
-</ul>
-</p>
-
-<h2>Acknowlegements</h2>
-
-<p>Thanks to
-<a href="http://cswww.essex.ac.uk/Research/FSS/projects/isawin/">Norbert Vöker</a>
-and <a href="http://www.abo.fi/~viorel.preoteasa/isabelle/">Viorel Preoteasa</a>
-whose efforts helped a lot to get Isabelle run this way.</p>
-
-<h2>Installing Cygwin</h2>
-
-<p>Cygwin is a POSIX emulation layer for Windows; it contains ports of a large
-collection of common Unix software (shells, perl, gcc, X11, latex, ImageMagick,
-…).</p>
-
-<p>To install it, get the installer from the
-<a href="http://www.cygwin.com">Cygwin website</a> and run it. It will ask you
-which packages to install, and then downloads and installs them.
-Please make sure you install everything needed by Isabelle; it is hard to give
-a concise list of packages here since the bundling of Cygwin packages may vary
-over time, but installing the base packages, perl, make, xemacs and x-server
-should be a good choice for the beginning.</p>
-
-<p>By default, cygwin installs to <tt>c:\cygwin</tt>; you may choose an arbitrary
-location, but it is recommended that it does not include any space or exotic
-characters. This directory will then become the root directory of the Cygwin
-filesystem tree, i.e. the Cygwin path <tt>/opt/smlnj</tt>
-will be mapped to Windows path <tt>c:\cygwin\opt\smlnj</tt>.</p>
-
-<p>After installation, open a Cygwin shell window (normally the installer
-makes a shortcut for you).</p>
-
-<h2>Getting and building SML/NJ</h2>
-
-<p>Now we are ready to get and build <a href="http://www.smlnj.org/">SML/NJ</a>;
-before this, set the environment variable SMLNJ_CYGWIN_RUNTIME to 1:
-
- <blockquote>
- <tt>
- export SMLNJ_CYGWIN_RUNTIME=1
- </tt>
- </blockquote>
-
- <blockquote>
- (or
- <tt>
- setenv SMLNJ_CYGWIN_RUNTIME 1
- </tt>
- for c shells).
- </blockquote>
-
-This setting will tell the build process that it should <em>not</em> attempt
-to build SML/NJ natively for Win32 but for Cygwin instead (see further
-<a href="http://smlnj.cs.uchicago.edu/dist/working/110.53/CYGWININSTALL">CYGWININSTALL</a>).</p>
-
-<p>So far, this setup was tested using the working version 110.53
-of SML/NJ from <a href="http://smlnj.cs.uchicago.edu/dist/working/110.53/">http://smlnj.cs.uchicago.edu/dist/working/110.53/</a>.
-SML/NJ provides a nice installer enabling you to download and build it.
-Read <a href="http://smlnj.cs.uchicago.edu/dist/working/110.53/INSTALL">INSTALL</a>
-to learn about the different possibilites to do this. The default packages
-should be sufficient.</p>
-
-<p>In the following, it is assumed that you install SML/NJ to Cygwin path <tt>/opt/smlnj</tt>;
-if you choose an other
-location, some tweaking in the <a href="#config"><tt>etc/settings</tt> file</a>
-may be neccessary later.</p>
-
-<p>Whenever SMLNJ is used, the SMLNJ_CYGWIN_RUNTIME environment variable
-must be set to 1 (later on a convenient mechanism to make this the default
-is proposed).</p>
-
-<h2>Installing Isabelle</h2>
-
-<p>Download the latest Isabelle and ProofGeneral <a href="packages.html">release packages</a>.
-Assuming that you are in the directory where
-you downloaded the files, install them into <tt>/opt</tt> by typing into the
-bash shell:
-
- <blockquote>
- <tt>
- tar -C /usr/opt -xvzf <!-- _GP_ href(distname . ".tar.gz", distname . ".tar.gz") --> <br>
- tar -C /usr/opt -xvzf <!-- _GP_ href("contrib/ProofGeneral.tar.gz", "ProofGeneral.tar.gz") --> <br>
- </tt>
- </blockquote>
-
-During extraction, one inconvenience may occur, see <a href="inconvenience">below</a>.</p>
-
-<p>The location <tt>/opt</tt> again is just a proposal; if you choose other
-locations, some tweaking in the <a href="#config"><tt>etc/settings</tt> file</a>
-may be neccessary later.</p>
-
-<h2 id="config">Configuring Isabelle</h2>
-
-<p>Edit the file <tt>/opt/Isabelle/etc/settings</tt>; first, uncomment the lines
-about SMLNJ. Also set the variable SMLNJ_CYGWIN_RUNTIME to 1, in order the
-cygwin version of SMLNJ is used. As mentioned above, the path variables for
-the ML system and ProofGeneral may need adjustions, depending on your different
-installation locations.</p>
-
-<p>Take heed of the setting of ISABELLE_HOME_USER; by default, this is
-<tt>~/isabelle</tt>. To detect which Windows path this will be mapped to,
-type into the Cygwin bash shell:
-
- <blockquote>
- <tt>
- cygpath --windows ~/isabelle
- </tt>
- </blockquote>
-
-If you don't like this location to be the isabelle home directory, consider
-setting of ISABELLE_HOME_USER to another value; use <tt>cygpath --unix
-<winpath></tt> to detect which Cygwin path a given Windows path is mapped to.</p>
-
-<p>A typical change could look like this:
-
- <blockquote>
- from<br/>
- <tt>
- # Standard ML of New Jersey 110 or later<br>
- #ML_SYSTEM=smlnj-110<br>
- #ML_HOME="$ISABELLE_HOME/../smlnj/bin"<br>
- #ML_OPTIONS="@SMLdebug=/dev/null"<br>
- #ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")<br>
- </tt>
- </blockquote>
-
- <blockquote>
- to<br/>
- <tt>
- # Standard ML of New Jersey 110 or later<br>
- SMLNJ_CYGWIN_RUNTIME=1<br>
- ML_SYSTEM=smlnj-110<br>
- ML_HOME="$ISABELLE_HOME/../smlnj/bin"<br>
- ML_OPTIONS="@SMLdebug=/dev/null"<br>
- ML_PLATFORM=$(eval $("$ML_HOME/.arch-n-opsys" 2>/dev/null); echo "$HEAP_SUFFIX")
- </tt>
- </blockquote>
-
-</p>
-
-<h2>Building logics</h2>
-
-<p>Now we can compile some logics. Start the cygwin shell (if not still
-running) and type:
-
- <blockquote>
- <tt>
- cd /opt/Isabelle<br>
- build HOL<br>
- build ZF
- </tt>
- </blockquote>
-</p>
-
-<p>The compilation process may take some time (depending on
-how fast the computer is). Before building a logic image the build
-program shows some variables and expects user input – just hit enter.
-
-<h2>Running Isabelle with ProofGeneral</h2>
-
-<p>On Linux, Isabelle can be started by two scripts located in <tt>Isabelle/bin</tt>:
-<tt>Isabelle</tt> and <tt>isabelle</tt>. <tt>Isabelle</tt> attempts to start
-ProofGeneral with XEmacs, and isabelle starts it in an SML shell session.
-However Windows treats the two names as one. To get around this just copy
-<tt>/opt/Isabelle/bin/isabelle</tt> to <tt>/opt/Isabelle/bin/Isabell</tt>.
-The script <tt>/opt/Isabelle/bin/Isabell</tt> will start Isabelle with ProofGeneral.</p>
-
-<p>Now everything should be ready. To test, start the cygwin shell and type
-
- <blockquote>
- <tt>startx &</tt>
- </blockquote>
-
-This will start the cygwin X server and an X shell window. In the X shell window,
-type
-
- <blockquote>
- <tt>/opt/Isabelle/bin/Isabell &</tt>.
- </blockquote>
-
-This will start the ProofGeneral interface for Isabelle. After a while
-an empty buffer <tt>Scratch.thy</tt> is created. You can turn on
-X-Symbol from the menu Proof-General &rarrow; Options.</p>
-
-<p>Load one of your favorite theories and test your Isabelle installation
-by proving something.</p>
-
-<p>To simplify starting ProofGeneral, consider writing a Windows command script,
-e.g.
-
- <blockquote>
- <tt>@bash startx -geometry 30x4 -iconic -e Isabell</tt>
- </blockquote>
-
-and assigning a shortcut in the start menu to it.</p>
-
-<h2 id="inconvenience">Inconveniencies with the current version of Isabelle</h2>
-
-<p>With the current Isabelle release (Isabelle 2004), there are two inconveniencies:
-<ul>
- <li>During extraction you will get a warning that file <tt>Real/HahnBanach/Aux.thy</tt>
- can not be created. This is because <tt>Aux</tt> is not allowed as a
- filename under Windows. If you do not want to run the HahnBanach example,
- you might simply want to ignore this warning.</li>
- <li>The tool <tt>isatool mkdir</tt> tries to detect the name of the current
- user, to put it into the generated <tt>root.tex</tt>. Alas, on Windows, this
- leads to an unquoted <tt>\</tt> in the TeX file. So you either must edit
- your <tt>root.tex</tt> manually to fix this, or directly patch <tt>/opt/Isabelle/lib/Tools/mkdir</tt>
- by replacing
-
- <blockquote>
- <tt>
- AUTHOR=$("$AUTO_PERL" -e "@pw = getpwnam(\"$USER\"); print @pw[6]" | tr _ -)
- </tt>
- </blockquote>
-
- with
-
- <blockquote>
- <tt>
- AUTHOR="default author name"
- </tt>
- </blockquote>
-
- </li>
-</ul>
-
-<p>To get around these inconveniencies, consider using a recent developer snapshot
-of Isabelle; both will be fixed in the next Isabelle release.</p>
-
-<h2 id="polyml">A note on Poly/ML</h2>
-
-<p>As indicated above, Isabelle does <em>not</em> run
-neatly with <a href="www.polyml.org/">Poly/ML</a> on Windows, for two
-reasons:
-<ul>
- <li>The native port of Poly/ML for Windows does not support shell-like stdin
- and stdout; instead, it implements
- its own »terminal«. Alas, all »higher«
- Isabelle features (Isar, ProofGeneral, …) depend on stdin and stdout.
- So, though on the pure ML level Isabelle may run, its usability will be
- very restricted.</li>
- <li>It is not clear how Poly/ML has to be compiled for Cygwin.</li>
-</ul>
-</p>
-
-<p>If you know how to circumvent (fully or partially) any of these problems,
-please let us know.</p>
-
--- a/Admin/page/dist-content/packages.content Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,141 +0,0 @@
-%title%
-Isabelle Packages
-
-%body%
-
-<p>
-
-The following source and binary packages of <!-- _GP_ distname -->
-provide everything required for easy installation of the full Isabelle
-working environment on common Unix platforms (e.g. Linux, Darwin, Solaris)
-
-<p>
-
-A <em>minimal</em> Isabelle installation requires only <tt>bash</tt>
-and <tt>perl</tt> (usually provided by the operating system), and a
-suitable implementation of Standard ML (e.g. <a
-href="http://www.polyml.org">Poly/ML</a> as included below). A
-<em>comfortable</em> Isabelle working environment demands further user
-interface support, as provided by <a
-href="http://proofgeneral.inf.ed.ac.uk/">Proof General</a> (please <a
-href="http://proofgeneral.inf.ed.ac.uk/register">register</a>). The Proof General
-distribution now includes the <a
-href="http://x-symbol.sourceforge.net">X-Symbol</a> package. It
-should be used with a recent version of <a
-href="http://www.xemacs.org">XEmacs 21</a> or <a
-href="http://www.gnu.org/software/emacs/emacs.html">GNU Emacs 21</a> (with
-Mule enabled).
-
-<p>
-
-
-<h2>Packages</h2>
-
-We provide a complete set of packages for Isabelle, Proof General, and
-PolyML.
-<p>
-While XEmacs 21 is not included here, most operating system
-distributions already provide a suitable package, although not
-installed by default. Some of the packages below are platform
-dependent; we include binaries for Linux/x86, Solaris/Sparc, and
-Darwin/PPC (MacOS X).
-<p>
-Short <a href="#install">installation instructions</a> are near the
-bottom of this page. For more information, see the file INSTALL in
-<!-- _GP_ distname -->.tar.gz.
-
-<p>
-
-<!-- _GP_ setdowncolor("\"#E0E0E0\"") -->
-<table border="0" cellspacing="5" cellpadding="4" width="520" style="margin: 0px auto 0px auto">
-
-<!-- _GP_ downloadhead("Isabelle") -->
-<!-- _GP_ download(1, "Sources and documentation", distname . ".tar.gz", "../..") -->
-<!-- _GP_ download(1, "Documentation in PDF", distname . "_pdf.tar.gz", "../..") -->
-<!-- _GP_ download(1, "Theory library in PDF and HTML", distname . "_library.tar.gz", "../..") -->
-
-<!-- _GP_ downloadhead("Proof General") -->
-<!-- _GP_ download(1, "Proof General", "contrib/ProofGeneral-3.5.tar.gz", "../..") -->
-
-<!-- _GP_ downloadhead("Poly/ML compiler and runtime system") -->
-<!-- _GP_ download(1, "Poly/ML base system", "contrib/polyml_base.tar.gz", "../..") -->
-<!-- _GP_ download(3, "Poly/ML binary modules", "contrib/polyml_x86-linux.tar.gz", "../..") -->
-<!-- _GP_ download(0, "", "contrib/polyml_sparc-solaris.tar.gz", "../..") -->
-<!-- _GP_ download(0, "", "contrib/polyml_ppc-darwin.tar.gz", "../..") -->
-
-<!-- _GP_ downloadhead("Precompiled logics") -->
-<!-- _GP_ download(3, "HOL", "HOL_x86-linux.tar.gz", "../..") -->
-<!-- _GP_ download(0, "", "HOL_sparc-solaris.tar.gz", "../..") -->
-<!-- _GP_ download(0, "", "HOL_ppc-darwin.tar.gz", "../..") -->
-<!-- _GP_ download(3, "HOL-Complex", "HOL-Complex_x86-linux.tar.gz", "../..") -->
-<!-- _GP_ download(0, "", "HOL-Complex_sparc-solaris.tar.gz", "../..") -->
-<!-- _GP_ download(0, "", "HOL-Complex_ppc-darwin.tar.gz", "../..") -->
-<!-- _GP_ download(3, "HOL4", "HOL4_x86-linux.tar.gz", "../..") -->
-<!-- _GP_ download(0, "", "HOL4_sparc-solaris.tar.gz", "../..") -->
-<!-- _GP_ download(0, "", "HOL4_ppc-darwin.tar.gz", "../..") -->
-<!-- _GP_ download(3, "ZF", "ZF_x86-linux.tar.gz", "../..") -->
-<!-- _GP_ download(0, "", "ZF_sparc-solaris.tar.gz", "../..") -->
-<!-- _GP_ download(0, "", "ZF_ppc-darwin.tar.gz", "../..") -->
-
-<!-- _GP_ downloadhead("HOL4 proof terms") -->
-<!-- _GP_ download(1, "HOL4 proof terms", "contrib/HOL4-proofs.tar.gz", "../..") -->
-</table>
-
-
-<p>
-
-<h2>Installation</h2>
-
-<a name="install">In</a> fact, there is no installation required. Users may just unpack all
-required packages within the same directory. The default settings of
-Isabelle should be reasonable for most circumstances.
-
-<p>
-
-A typical Linux/x86 site installation of Isabelle/HOL works as
-follows. By using GNU <tt>tar</tt>, the archives are uncompressed and
-unpacked into the <tt>/usr/local</tt> directory (this location may be
-changed to anything appropriate).
-
-<p>
-
-<tt>
- tar -C /usr/local -xzf
-<!-- _GP_ href(distname . ".tar.gz", distname . ".tar.gz") --> <br>
- tar -C /usr/local -xzf
-<!-- _GP_ href("contrib/ProofGeneral.tar.gz", "ProofGeneral.tar.gz") --> <br>
- tar -C /usr/local -xzf
-<!-- _GP_ href("contrib/polyml_base.tar.gz", "polyml_base.tar.gz") --> <br>
- tar -C /usr/local -xzf
-<!-- _GP_ href("contrib/polyml_x86-linux.tar.gz", "polyml_x86-linux.tar.gz") --> <br>
- tar -C /usr/local -xzf
-<!-- _GP_ href("HOL_x86-linux.tar.gz", "HOL_x86-linux.tar.gz") --> <br>
-</tt>
-
-<p>
-
-Users may now invoke Isabelle without further ado, e.g. run the main
-executable <tt>/usr/local/Isabelle/bin/Isabelle</tt> to launch the
-Proof General interface for Isabelle/Isar. Note that there is a
-separate option in the Proof General <em>Options</em> menu to enable
-X-Symbol.
-
-<p>
-
-If Emacs appears to hang when the prover process is started, see the
-<A HREF="http://proofgeneral.inf.ed.ac.uk/FAQ">Proof General FAQ</a>
-for advice.
-
-<h3>Other platforms</h3>
-
-<p>Although Isabelle is natively designed for Unix environments
-(e.g. Solaris, Linux), it may also run under similar, Unix-like
-platforms. The following installation instructions are hints
-contributed by Isabelle users. Feel free to contact us for any
-suggestions, corrections or improvements.</p>
-
- <ul>
- <li><a href="notes_macos_darwin.html">Installation notes for Mac OS X</a></li>
- <li><a href="notes_win_cygwin.html">Installation notes for Cygwin/Windows</a></li>
- </ul>
-
--- a/Admin/page/dist-content/past.content Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,22 +0,0 @@
-%title%
-Isabelle Past Releases
-
-%body%
-<p>
-
-Past releases of Isabelle are available from the Cambridge archive:
-
-<ul>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle2003.tar.gz">Isabelle2003</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle2002.tar.gz">Isabelle2002</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle99-2.tar.gz">Isabelle99-2</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle99-1.tar.gz">Isabelle99-1</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle99.tar.gz">Isabelle99</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle98-1.tar.gz">Isabelle98-1</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle98.tar.gz">Isabelle98</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94-8.tar.gz">Isabelle94-8</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94-7.tar.gz">Isabelle94-7</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94-6.tar.gz">Isabelle94-6</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle94.tar.gz">Isabelle94</a></li>
-<li><a href="http://www.cl.cam.ac.uk/users/lcp/archive/Isabelle93.tar.gz">Isabelle93</a></li>
-</ul>
--- a/Admin/page/dist-layout/navigation.html Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,14 +0,0 @@
-<div style="text-align: center; margin-top: 30px; margin-bottom: 45px">
-<a href="index.html"><img src="isabelle.gif" width="100" height="86" alt="[Isabelle logo]" border="0"></a>
-<div style="font-weight: bold; margin-top: 10px">Isabelle Distribution Area</div>
-</div>
-<!-- _GP_ setnavcolor("#F0F0F0") -->
-<!-- _GP_ page("Mirrors", "index") -->
-<!-- _GP_ empty_line(3) -->
-<!-- _GP_ page("Packages", "packages") -->
-<!-- _GP_ empty_line(3) -->
-<!-- _GP_ page("Documentation", "docs") -->
-<!-- _GP_ empty_line(3) -->
-<!-- _GP_ page("Past Releases", "past") -->
-<!-- _GP_ empty_line(3) -->
-
--- a/Admin/page/dist-layout/template.html Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,63 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
-<html>
- <!-- _GP_ include("$pwd/common/functions.pl") -->
- <head>
- <title> <!-- _GP_ content("title") --> </title>
- <META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">
- <LINK REL="SHORTCUT ICON" HREF="favicon.ico">
- <!-- _GP_ content("meta") -->
- </head>
-
- <body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040">
-
- <table border="0" cellspacing="5" width="100%">
-
- <tr>
- <td width="188" valign="top" bgcolor="#A8A8CF">
- <!-- _GP_ include("$pwd/dist-layout/navigation.html") -->
- <table height="20"><tr><td> </td></tr></table>
- </td>
-
- <td width="100%" valign="top">
-
- <center>
- <table width="70%" border="0" cellspacing="10" cellpadding="10">
- <tr>
- <td align="center" bgcolor="#A8A8CF">
- <b>
- <font face="Arial,Helvetica" size="+2"><!-- _GP_ content("title") --></font>
- </b>
- </td>
- </tr>
- </table>
- </center>
-
- <p>
-
- <center>
- <table width="99%" border="0" cellspacing="0" cellpadding="10">
- <tr>
- <td align="left">
- <!-- _GP_ content("body") -->
- </td>
- </tr>
- </table>
- </center>
- </td>
- </tr>
-
- <tr>
- <td align="right" colspan="2" height="20">
- <table border="0" cellpadding="4" cellspacing="0">
- <tr><td>
- <font size="-1" face="helvetica, arial">
- last update at <!-- _GP_ when -->
- </font>
- </td></tr>
- </table>
- </td>
- </tr>
-
- </table>
- </body>
-</html>
Binary file Admin/page/main-content/PG-preview.pdf has changed
Binary file Admin/page/main-content/cambridge.gif has changed
--- a/Admin/page/main-content/docs.content Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-%title%
-Isabelle Documentation
-
-%body%
-
-<!-- _GP_ distname --> documentation is included here as browsable PDF
-for convenience. These documents are also part of the standard
-Isabelle <a href="dist/index.html">distribution</a>. For getting
-started with Isabelle quickly, we recommend the
-<a href="dist/<!-- _GP_ distname -->/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="http://isabelle.in.tum.de/coursematerial/">course material</a>
-page. See the
-<a href="faq.html">FAQ</a> for answers to frequent problems.
-
-<!-- _GP_ include("$pwd/docu-contents.main") -->
--- a/Admin/page/main-content/faq.content Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,322 +0,0 @@
-%title%
-Isabelle FAQ
-
-%meta%
-<style type="text/css">
- <!--
- .question { background-color:#C0C0C0; color:#000001; padding:3px; margin-top:12px; font-weight: bold; }
- .answer { background-color:#E0E0E0; padding:3px; margin-top:3px; }
- -->
-</style>
-
-
-%body%
- <h2>General Questions</h2>
- <table class="question" width="100%">
- <tr>
- <td>What is Isabelle?</td>
- </tr>
- </table>
-
- <table class="answer" width="100%">
- <tr><td>Isabelle is a popular generic theorem proving
- environment developed at Cambridge University (<a
- href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>)
- and TU Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias
- Nipkow</a>). See the <a
- href="http://isabelle.in.tum.de/">Isabelle homepage</a> for
- more information.</td></tr>
- </table>
-
-
- <table class="question" width="100%">
- <tr>
- <td>Where can I find documentation?</td>
- </tr>
- </table>
- <table class="answer" width="100%">
- <tr><td><a href="http://isabelle.in.tum.de/docs.html">This
- way, please</a>. Also have a look at the <a
- href="http://isabelle.in.tum.de/library/">theory
- library</a>.</td></tr>
- </table>
-
- <table class="question" width="100%">
- <tr>
- <td>Is it available for download?</td>
- </tr>
- </table> <table class="answer" width="100%"> <tr><td>Yes, it is
- available from <a
- href="http://isabelle.in.tum.de/dist/">several mirror
- sites</a>. It should run on most recent Unix systems (Solaris,
- Linux, MacOS X, etc.).</td></tr>
- </table>
-
-
- <h2>Syntax</h2>
- <table class="question" width="100%">
- <tr>
- <td>There are lots of arrows in Isabelle. What's the
- difference between <tt>-></tt>, <tt>=></tt>, <tt>--></tt>,
- and <tt>==></tt> ?</td>
- </tr>
- </table>
- <table class="answer" width="100%">
- <tr><td>Isabelle uses the <tt>=></tt> arrow for the function
- type (contrary to most functional languages which use
- <tt>-></tt>). So <tt>a => b</tt> is the type of a function
- that takes an element of <tt>a</tt> as input and gives you an
- element of <tt>b</tt> as output. The long arrow <tt>--></tt>
- and <tt>==></tt> are object and meta level
- implication. Roughly speaking, the meta level implication
- should only be used when stating theorems where it separates
- the assumptions from the conclusion. Whenever you need an
- implication inside a HOL formula, use <code>--></code>.
- </td></tr>
- </table>
-
- <table class="question" width="100%"><tr><td>Where do I have to put those double quotes?</td></tr></table>
-
- <table class="answer" width="100%"><tr><td>Isabelle distinguishes between <em>inner</em>
- and <em>outer</em> syntax. The outer syntax comes from the
- Isabelle framework, the inner syntax is the one in between
- quotation marks and comes from the object logic (in this case HOL).
- With time the distinction between the two becomes obvious, but in
- the beginning the following rules of thumb may work: types should
- be inside quotation marks, formulas and lemmas should be inside
- quotation marks, rules and equations (e.g. for definitions) should
- be inside quotation marks, commands like <tt>lemma</tt>,
- <tt>consts</tt>, <tt>primrec</tt>, <tt>constdefs</tt>,
- <tt>apply</tt>, <tt>done</tt> are without quotation marks, as are
- the names of constants in constant definitions (<tt>consts</tt>
- and <tt>constdefs</tt>)
- </td></tr></table>
-
- <table class="question" width="100%"><tr><td>What is <tt>"No such
- constant: _case_syntax"</tt> supposed to tell
- me?</td></tr></table>
-
- <table class="answer" width="100%"><tr><td>You get this message if
- you use a case construct on a datatype and have a typo in the
- names of the constructor patterns or if the order of the
- constructors in the case pattern is different from the order in
- which they where defined (in the datatype definition).
- </td></tr></table>
-
- <table class="question" width="100%"><tr><td>Why doesn't Isabelle understand my
- equation?</td></tr></table>
-
- <table class="answer" width="100%"><tr><td>Isabelle's equality <tt>=</tt> binds
- relatively strongly, so an equation like <tt>a = b & c</tt> might
- not be what you intend. Isabelle parses it as <tt>(a = b) &
- c</tt>. If you want it the other way around, you must set
- explicit parentheses as in <tt>a = (b & c)</tt>. This also applies
- to e.g. <tt>primrec</tt> definitions (see below).</td></tr></table>
-
- <table class="question" width="100%"><tr><td>What does it mean "not a proper
- equation"?</td></tr></table>
-
- <table class="answer" width="100%"><tr><td>Most commonly this is an instance of the
- question above. The <tt>primrec</tt> command (and others) expect
- equations as input, and since equality binds strongly in Isabelle,
- something like <tt>f x = b & c</tt> is not what you might expect
- it to be: Isabelle parses it as <tt>(f x = b) & c</tt> (which is
- indeed not a proper equation). To turn it into an equation you
- must set explicit parentheses: <tt>f x = (b & c)</tt>.</td></tr></table>
-
- <table class="question" width="100%"><tr><td>What does it mean
- "<tt>Not a meta-equality (==)</tt>"?</td></tr></table>
-
- <table class="answer" width="100%"><tr><td>This usually occurs if
- you use <tt>=</tt> for <tt>constdefs</tt>. The <tt>constdefs</tt>
- and <tt>defs</tt> commands expect not equations, but meta
- equivalences. Just use the <tt>\<equiv></tt> or <tt>==</tt>
- signs instead of <tt>=</tt>. </td></tr></table>
-
-
- <h2>Proving</h2>
-
- <table class="question" width="100%"><tr><td>What does "empty result sequence"
- mean?</td></tr></table>
-
- <table class="answer" width="100%"><tr><td>It means that the applied proof method (or
- tactic) was unsuccessful. It did not transform the goal in any
- way, or simply just failed to do anything. You must try another
- tactic (or give the one you used more hints or lemmas to work
- with)</td></tr></table>
-
-
- <table class="question" width="100%"><tr><td>The Simplifier doesn't want to apply my
- rule, what's wrong?</td></tr></table>
-
- <table class="answer" width="100%"><tr><td>
- Most commonly this is a typing problem. The rule you want to apply
- may require a more special (or just plain different) type from
- what you have in the current goal. Use the ProofGeneral menu
- <tt>Isabelle/Isar -> Settings -> Show Types</tt> and the
- <tt>thm</tt> command on the rule you want to apply to find out if
- the types are what you expect them to be (also take a look at the
- types in your goal). <tt>Show Sorts</tt>, <tt>Show Constants</tt>,
- and <tt>Trace Simplifier</tt> in the same menu may also be
- helpful.
- </td></tr></table>
-
-
- <table class="question" width="100%"><tr><td>If I do <tt>auto</tt>, it leaves me a goal
- <tt>False</tt>. Is my theorem wrong?</td></tr></table>
-
- <table class="answer" width="100%"><tr><td>Not necessarily. It just means that
- <tt>auto</tt> transformed the goal into something that is not
- provable any more. That could be due to <tt>auto</tt> doing
- something stupid, or e.g. due to some earlier step in the proof
- that lost important information. It is of course also possible
- that the goal was never provable in the first place.</td></tr></table>
-
-
- <table class="question" width="100%"><tr><td>Why does <tt>lemma
- "1+1=2"</tt> fail?</td></tr></table>
-
- <table class="answer" width="100%"><tr><td>Because it is not
- necessarily true. Isabelle does not assume that 1 and 2 are
- natural numbers. Try <tt>"(1::nat)+1=2"</tt>
- instead.</td></tr></table>
-
-
- <table class="question" width="100%"><tr><td>Can Isabelle find
- counterexamples?</td></tr></table>
-
- <table class="answer" width="100%"><tr><td>
- <p>
- For arithmetic goals, <code>arith</code> finds counterexamples.
- For executable goals, <code>quickcheck</code> tries to find a
- counterexample. For goals of a more logical nature (including
- quantifiers, sets and inductive definitions) <code>refute</code>
- searches for a countermodel.
- </p>
- <p>
- Otherwise, negate the proposition
- and instantiate (some) variables with concrete values. You may
- also need additional assumptions about these values. For example,
- <tt>True & False ~= True | False</tt> is a counterexample of <tt>A
- & B = A | B</tt>, and <tt>A = ~B ==> A & B ~= A | B</tt> is
- another one. Sometimes Isabelle can help you to find the
- counterexample: just negate the proposition and do <tt>auto</tt>
- or <tt>simp</tt>. If lucky, you are left with the assumptions you
- need for the counterexample to work.
- </p>
- </td></tr></table>
-
-
- <h2>Interface</h2>
-
- <table class="question" width="100%"><tr><td>ProofGeneral appears to hang when Isabelle is started.</td></tr></table>
-
- <table class="answer" width="100%"><tr>This may be because of UTF-8 issues e.g. in Red Hat 8.0/9.0, Suse 9.0/9.1
- <p>
- RedHat 8 and later has glibc 2.2 and UTF8 encoded output may be
- turned on in default locale. Unfortunately Proof General relies on
- 8-bit characters which are UTF8 prefixes in the output of proof
- assistants (inc Coq, Isabelle). These prefix characters are not
- flushed to stdout individually. As a workaround we must find a way
- to disable interpretation of UTF8 in the C libraries that Coq and
- friends use.
- <p>
- Doing this inside PG/Emacs seems tricky; locale settings are
- set/inherited in strange ways. One solution is to run the Emacs
- process itself with an altered locale setting, for example,
- starting XEmacs by typing:
- <p>
- <tt>$ LC_CTYPE=en_GB Isabelle &</tt>
- <p>
- The supplied proofgeneral script makes this setting if it sees
- the string UTF in the current value of LC_CTYPE. Depending on your
- distribution, this variable might also be called <tt>LANG</tt>.
- <p>
- Alternatively you can set LC_CTYPE or LANG inside a file ~/.i18n, which will
- be read by the shell. This will affect all applications, though.
- [ suggestions for a better workaround inside Emacs would be welcome ]
- <p>
- NB: a related issue is warnings from x-symbol: "Emacs language
- environment and system locale specify different encoding, I'll
- assume `iso-8859-1'". This warning appears to be mainly harmless.
- Notice that the variable `buffer-file-coding-system' may determine
- the format that files are saved in.<td></td></tr></table>
-
- <table class="question" width="100%"><tr><td>X-Symbol doesn't seem to work. What can I
- do?</td></tr></table>
-
- <table class="answer" width="100%"><tr><td>The most common reason why X-Symbol doesn't
- work is: it's not switched on yet. Assuming you are using
- ProofGeneral and have installed the X-Symbol package, you still
- need to turn X-Symbol on in ProofGeneral: select the menu items
- <tt>Proof-General -> Options -> X-Symbol</tt> and (if you want to
- save the setting for future sessions) select <tt>Options -> Save
- Options</tt> in XEmacs.</td></tr></table>
-
- <table class="question" width="100%"><tr><td>How do I input those X-Symbols anyway?</td></tr></table>
-
- <table class="answer" width="100%"><tr><td>
- There are lots of ways to input x-symbols. The one that always
- works is writing it out in plain text (e.g. for the 'and' symbol
- type <tt>\<and></tt>). For common symbols you can try to "paint
- them in ASCII" and if the xsymbol package recognizes them it will
- automatically convert them into their graphical
- representation. Examples: <tt>--></tt> is converted into the long
- single arrow, <tt>/\</tt> is converted into the 'and' symbol, the
- sequence <tt>=_</tt> into the equivalence sign, <tt><_</tt> into
- less-or-equal, <tt>[|</tt> into opening semantic brackets, and so
- on. For greek characters, the <code>rotate</code> command works well:
- to input α type <code>a</code> and then <code>C-.</code>
- (control and <code>.</code>). You can also display the
- grid-of-characters in the x-symbol menu to get an overview of the
- available graphical representations (not all of them already have
- a meaning in Isabelle, though).
- </td></tr></table>
-
- <h2>System</h2>
-
- <table class="question" width="100%"><tr><td>I want to generate one of those flashy LaTeX
- documents. How?</td></tr></table>
-
- <table class="answer" width="100%"><tr><td>You will need to work with the
- <tt>isatool</tt> command for this (in a Unix shell). The easiest
- way to get to a document is the following: use <tt>isatool
- mkdir</tt> to set up a new directory. The command will also create
- a file called <tt>IsaMakefile</tt> in the current directory. Put
- your theory file(s) into the new directory and edit the file
- <tt>ROOT.ML</tt> in there (following the comments) to tell
- Isabelle which of the theories to load (and in which order). Go
- back to the parent directory (where the <tt>IsaMakefile</tt> is)
- and type <tt>isatool make</tt>. Isabelle should then process your
- theories and tell you where to find the finished document. For
- more information on generating documents see the Isabelle Tutorial, Chapter 4.
- </td></tr></table>
-
-
- <table class="question" width="100%"><tr><td>I have a large formalization with many
- theories. Must I process all of them all of the time?</td></tr></table>
-
- <table class="answer" width="100%"><tr><td>No, you can tell Isabelle to build a so-called
- heap image. This heap image can contain your preloaded
- theories. To get one, set up a directory with a <tt>ROOT.ML</tt>
- file (as for generating a document) and use the command
- <tt>isatool usedir -b HOL MyImage</tt> in that directory to create
- an image <tt>MyImage</tt> using the parent logic <tt>HOL</tt>.
- You should then be able to invoke Isabelle with <tt>Isabelle -l
- MyImage</tt> and have everything that is loaded in ROOT.ML
- instantly available.</td></tr></table>
-
- <table class="question" width="100%"><tr><td>Does Isabelle run on Windows?</td></tr></table>
-
- <table class="answer" width="100%"><tr><td> After a fashion, yes,
- but Isabelle is not being developed for Windows. A friendly user
- (Norbert Völker) has managed to get a minimal Isabelle environment
- to work on it. See the description on <a
- href="http://cswww.essex.ac.uk/Research/FSS/projects/isawin/">his
- website</a>. Be warned, though: emphasis is on <em>minimal</em>,
- working with Windows is no fun at all. To enjoy Isabelle in its
- full beauty it is recommended to get a Linux distribution (they
- are inexpensive, any reasonably recent one should work, dualboot
- Windows/Linux should pose no problems).
- </td></tr></table>
-
Binary file Admin/page/main-content/favicon.ico has changed
--- a/Admin/page/main-content/index.content Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,138 +0,0 @@
-%title%
-Isabelle
-
-%body%
-
-<p>
-
-<h2>What is Isabelle?</h2>
-
-Isabelle is a popular generic theorem proving environment developed at
-Cambridge University (<a
-href="http://www.cl.cam.ac.uk/users/lcp/">Larry Paulson</a>) and TU
-Munich (<a href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>).
-See the <a href="overview.html">Isabelle overview</a>.
-
-<p>
-
-These pages provide general information on Isabelle, more specific
-information is available from the local pages
-
-<ul>
-
-<li><a
-href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><strong>Isabelle
-at Cambridge</strong></a>
-
-<li><a href="http://www4.in.tum.de/proj/theoremprov/group.html"><strong>Isabelle
-at Munich</strong></a>
-
-</ul>
-
-See there for information on projects done with Isabelle, mailing list
-archives, research papers, the Isabelle bibliography, and Isabelle
-workshops and courses.
-
-<p>
-
-<h2>Isabelle 2005 - Preview</h2>
-
-<ul>
-<li>New commands for instantiating locales</li>
-<li>New command for finding matching rewrite rules</li>
-<li>Finding theorems by term patterns</li>
-<li>New automatic transitivity reasoner</li>
-<li>New command for ad-hoc theory viewing and printing</li>
-<li>Much extended and improved theory of finite sets</li>
-<li>New syntax that will allow > and >= in addition to < and <=</li>
-</ul>
-
-<h2>Contributing</h2>
-
-Did you have to prove a lemma that should have been part of the
-Isabelle distribution? Send it to us! <p> We will collect theorems
-sent to <a
-href="mailto:isabelle-lemmas@cl.cam.ac.uk">isabelle-lemmas@cl.cam.ac.uk</a>.
-Accepted material will be included in the Isabelle sources, with
-credit given to the author. Note that the Isabelle sources are
-distributed under the BSD license. Lemmas should be general, useful,
-and not too large. For larger developments you might want to consider
-a submission to the <a href="http://afp.sf.net">Archive of Formal
-Proofs</a>.
-
-
-<h2>Course Material, Exercises</h2>
-
-The <a
-href="http://isabelle.in.tum.de/coursematerial/">course material</a>
-page makes slides, demos, and exercises of a growing number of
-Isabelle courses available. It is meant as a resource for people
-who would like to learn Isabelle as well as for those who would like
-to teach it.
-
-<p>
-
-<h2>AFP - The Archive of Formal Proofs</h2>
-
-The <a href="http://afp.sf.net">Archive of Formal Proofs</a> is a
-collection of proof libraries, examples, and larger scientifc
-developments, mechanically checked in Isabelle. It is organized in the
-way of a scientific journal. Submissions are refereed.
-
-<p>
-
-<h2><!-- _GP_ distname --></h2>
-New features in <strong><!-- _GP_ distname --></strong> include
-<ul>
-<li>New image HOL4 with imported library from HOL4 system on top of
- HOL-Complex (about 2500 additional theorems).</li>
-
-<li>New theory Ring_and_Field with over 250 basic numerical laws,
- all proved in axiomatic type classes for semirings, rings and fields.</li>
-
-<li>New locale <code>ring</code> for non-commutative rings in HOL-Algebra.</li>
-
-<li>Type <code>rat</code> of the rational numbers available in HOL-Complex.</li>
-
-<li>New theory of matrices with an application to linear programming in HOL-Matrix.</li>
-
-<li>Improved locales (named proof contexts), instantiation of locales.</li>
-
-<li>Improved handling of linear and partial orders in simplifier.</li>
-
-<li>New <code>specification</code> command for definition by specification.</li>
-
-<li>New Isar command <code>finalconsts</code> prevents constants being given a definition later.</li>
-
-<li><code>arith</code> now generates counterexamples for reals as well.</li>
-
-<li>New <code>quickcheck</code> command
- to search for counterexamples of executable goals.
- (see HOL/ex/Quickcheck_Examples.thy)</li>
-<li>New <code>refute</code> command
- to search for finite countermodels of goals.
- (see HOL/ex/Refute_Examples.thy)
-</li>
-
-<li>Presentation and x-symbol enhancements, greek letters and
-sub/superscripts allowed in identifiers.</li>
-</ul>
-<a href="dist/<!-- _GP_ distname -->/NEWS">[Complete Changelog]</a>
-<p>
-The <strong><!-- _GP_ distname --></strong> distribution is available
-from several <a href="dist/index.html">mirror sites</a>. It includes
-source and binary packages and browsable documentation. You can also
-browse the <a href="library/index.html">Isabelle theory library</a>
-online. For the curious, there is a nightly generated <a
-href="http://isabelle.in.tum.de/devel/">development snapshot</a>
-available.
-
-<p>
-
-<h2>Mailing list</h2>
-
-Use the mailing list <a
-href="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a>
-and its <a href="http://www.cl.cam.ac.uk/users/lcp/archive/">archive</a> to
-discuss problems and results. To subscribe, <a href="mailto:lcp@cl.cam.ac.uk?subject=subscribe&body=Please%20add%20me%20to%20the%20Isabelle%20mailing%20list">contact Larry Paulson</a>.
-
Binary file Admin/page/main-content/isabelle-lemmas.gif has changed
--- a/Admin/page/main-content/logics.content Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,109 +0,0 @@
-%title%
-Isabelle's Logics
-
-%body%
-
-Isabelle can be viewed from two main perspectives. On the one hand it
-may serve as a generic framework for rapid prototyping of deductive
-systems. On the other hand, major existing logics like
-<strong>Isabelle/HOL</strong> provide a theorem proving environment
-ready to use for sizable applications.
-
-
-<h2>Isabelle's Logics</h2>
-
-The Isabelle distribution includes a large body of object logics and
-other examples (see the <a href="library/index.html">Isabelle theory
-library</a>).
-
-<dl>
-
-<dt><a
-href="library/HOL/index.html"><strong>Isabelle/HOL</strong></a><dd> is
-a version of classical higher-order logic resembling that of the <A
-HREF="http://www.cl.cam.ac.uk/Research/HVG/HOL/">HOL System</A>. The
-main libraries of the HOL 4 System are now <a
-href="library/HOL/HOL-Complex/HOL4/index.html">available in
-Isabelle</a>.
-
-<dt><a
-href="library/HOLCF/index.html"><strong>Isabelle/HOLCF</strong></a><dd>
-adds Scott's Logic for Computable Functions (domain theory) to HOL.
-
-<dt><a
-href="library/FOL/index.html"><strong>Isabelle/FOL</strong></a><dd>
-provides basic classical and intuitionistic first-order logic. It is
-polymorphic.
-
-<dt><a
-href="library/ZF/index.html"><strong>Isabelle/ZF</strong></a><dd>
-offers a formulation of Zermelo-Fraenkel set theory on top of FOL.
-
-</dl>
-
-<p>
-
-Isabelle/HOL is currently the best developed object logic, including
-an extensive library of (concrete) mathematics, and various packages
-for advanced definitional concepts (like (co-)inductive sets and
-types, well-founded recursion etc.). The distribution also includes
-some large applications, for example correctness proofs of
-cryptographic protocols (<a
-href="library/HOL/Auth/index.html">HOL/Auth</a>) or communication
-protocols (<a href="library/HOLCF/IOA/index.html">HOLCF/IOA</a>).
-
-<p>
-
-Isabelle/ZF provides another starting point for applications, with a
-slightly less developed library. Its definitional packages are
-similar to those of Isabelle/HOL. Untyped ZF provides more advanced
-constructions for sets than simply-typed HOL.
-
-<p>
-
-There are a few minor object logics that may serve as further
-examples: <a href="library/CTT/index.html">CTT</a> is an extensional
-version of Martin-Löf's Type Theory, <a
-href="library/Cube/index.html">Cube</a> is Barendregt's Lambda Cube.
-There are also some sequent calculus examples under <a
-href="library/Sequents/index.html">Sequents</a>, including modal and
-linear logics. Again see the <a href="library/index.html">Isabelle
-theory library</a> for other examples.
-
-
-<h3>Defining Logics</h3>
-
-Logics are not hard-wired into Isabelle, but formulated within
-Isabelle's meta logic: <strong>Isabelle/Pure</strong>. There are
-quite a lot of syntactic and deductive tools available in generic
-Isabelle. Thus defining new logics or extending existing ones
-basically works as follows:
-
-<ol>
-
-<li>declare concrete syntax (via mixfix grammar and syntax macros),
-
-<li>declare abstract syntax (as higher-order constants),
-
-<li>declare inference rules (as meta-logical propositions),
-
-<li>instantiate generic automatic proof tools (simplifier, classical
-tableau prover etc.),
-
-<li>manually code special proof procedures (via tacticals or
-hand-written ML).
-
-</ol>
-
-The first three steps above are fully declarative and involve no ML
-programming at all. Thus one already gets a decent deductive
-environment based on primitive inferences (by employing the built-in
-mechanisms of Isabelle/Pure, in particular higher-order unification
-and resolution).
-
-For sizable applications some degree of automated reasoning is
-essential. Instantiating existing tools like the classical tableau
-prover involves only minimal ML-based setup. One may also write
-arbitrary proof procedures or even theory extension packages in ML,
-without breaching system soundness (Isabelle follows the well-known
-<em>LCF system approach</em> to achieve a secure system).
Binary file Admin/page/main-content/munich.gif has changed
--- a/Admin/page/main-content/overview.content Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,69 +0,0 @@
-%title%
-Isabelle overview
-
-%body%
-
-<p>
-<a href="http://isabelle.in.tum.de/">Isabelle</a> is a generic proof
-assistant. It allows mathematical formulas to be expressed in a formal
-language and provides tools for proving those formulas in a logical
-calculus. The main application is the formalization of mathematical proofs
-and in particular <em>formal verification</em>, which includes proving the
-correctness of computer hardware or software and proving properties of
-computer languages and protocols.
-</p>
-
-<p>Compared with similar tools, Isabelle's distinguishing feature is
-its flexibility. Most proof assistants are built around a single
-formal calculus, typically higher-order logic. Isabelle has the
-capacity to accept a variety of formal calculi. The distributed
-version supports higher-order logic but also axiomatic set theory and
-several <a href="logics.html">other formalisms</a>. Isabelle provides
-excellent notational support: new notations can be introduced, using
-normal mathematical symbols. Proofs can be written in a structured
-notation based upon traditional proof style, or more straightforwardly
-as sequences of commands. Definitions and proofs may include TeX
-source, from which Isabelle can automatically generate typeset
-documents.</p>
-
-<p>The main limitation of all such systems is that proving theorems
-requires much effort from an expert user. Isabelle incorporates some
-tools to improve the user's productivity by automating some parts of
-the proof process. In particular, Isabelle's <em>classical
-reasoner</em> can perform long chains of reasoning steps to prove
-formulas. The <em>simplifier</em> can reason with and about equations.
-Linear <em>arithmetic</em> facts are proved automatically. Isabelle is
-closely integrated with the <a
-href="http://proofgeneral.inf.ed.ac.uk/">Proof
-General</a> user interface, which eases the task of writing and
-maintaining proof scripts. </p>
-
-A hyperlinked <a href="PG-preview.mov">preview</a> demonstrating Isabelle and Proof
-General is provided in
-<a href="http://www.apple.com/quicktime/download/">QuickTime format</a>,
-and also as a non-hyperlinked <a href="PG-preview.pdf">PDF file</a>.
-
-<p>Isabelle comes with large theories of formally verified
-mathematics, including elementary number theory (for example, Gauss's
-law of quadratic reciprocity), analysis (basic properties of limits,
-derivatives and integrals), algebra (up to Sylow's theorem) and set
-theory (the relative consistency of the Axiom of Choice). Also
-provided are numerous examples arising from research into formal
-verification. Isabelle is <a href="dist/">distributed</a> free of
-charge to academic users.</p>
-
-<p>Ample <a href="dist/docs.html">documentation</a> is available,
-including a <a
-href="http://www4.in.tum.de/~nipkow/LNCS2283/">Tutorial</a> published
-by Springer-Verlag. Several <a
-href="http://www.cl.cam.ac.uk/users/lcp/papers/isabelle.html">papers</a>
-on the design of Isabelle are available. There is also a list of past
-and present <a
-href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/projects.html">projects</a>
-undertaken using Isabelle. </p>
-
-<p>Isabelle is a joint project between <a
-href="http://www.cl.cam.ac.uk/users/lcp/">Lawrence C. Paulson</a>
-(University of Cambridge, UK) and <a
-href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a> (Technical
-University of Munich, Germany).</p>
--- a/Admin/page/main-layout/navigation.html Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,17 +0,0 @@
-<div style="text-align: center; margin-top: 30px; margin-bottom: 45px">
-<a href="index.html">
- <img src="isabelle.gif" width="100" height="86" alt="[Isabelle logo]" border="0">
-</a>
-</div>
-<!-- _GP_ setnavcolor("#F0F0F0") -->
-<!-- _GP_ page("Home", "index") -->
-<!-- _GP_ empty_line(3) -->
-<!-- _GP_ page("Overview", "overview") -->
-<!-- _GP_ empty_line(3) -->
-<!-- _GP_ page("Logics", "logics") -->
-<!-- _GP_ empty_line(3) -->
-<!-- _GP_ page("Documentation", "docs") -->
-<!-- _GP_ empty_line(3) -->
-<!-- _GP_ page("Download", "dist/index") -->
-<!-- _GP_ empty_line(3) -->
-
--- a/Admin/page/main-layout/template.html Mon Jun 06 14:12:07 2005 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +0,0 @@
-<!DOCTYPE HTML PUBLIC "-//IETF//DTD HTML//EN">
-<html>
- <!-- _GP_ include("$pwd/common/functions.pl") -->
- <head>
- <title> <!-- _GP_ content("title") --> </title>
- <META HTTP-EQUIV="Content-Type" CONTENT="text/html; charset=iso-8859-1">
- <LINK REL="SHORTCUT ICON" HREF="favicon.ico">
- <!-- _GP_ content("meta") -->
- </head>
-
- <body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040">
-
- <table border="0" cellspacing="5" width="100%">
-
- <tr>
- <td width="188" valign="top" bgcolor="#608080">
- <!-- _GP_ include("$pwd/main-layout/navigation.html") -->
- <table height="20"><tr><td> </td></tr></table>
- </td>
-
- <td width="100%" valign="top">
-
- <div style="text-align: center">
- <table width="95%" border="0" cellspacing="10" cellpadding="10">
- <tr>
- <td width="60%" align="center" bgcolor="#aacccc">
- <b>
- <font face="Arial,Helvetica" size="+2"><!-- _GP_ content("title") --></font>
- </b>
- </td>
- <td width="40%" valign="middle" align="center" nowrap>
- <a href="http://www4.in.tum.de/proj/theoremprov/group.html"><img src="munich.gif"
- border=0 width="48" height="59" alt="[Munich logo]"></a>
-
- <a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><img
- src="cambridge.gif" width="150" height="49" border=0 alt="[Cambridge logo]"></a>
- </td>
- </tr>
- </table>
- </div>
-
- <p>
-
- <div style="text-align: center">
- <table width="99%" border="0" cellspacing="0" cellpadding="10">
- <tr>
- <td align="left">
- <!-- _GP_ content("body") -->
- </td>
- </tr>
- </table>
- </div>
- </td>
- </tr>
-
- <tr>
- <td align="right" colspan="2" height="20">
- <table border="0" cellpadding="4" cellspacing="0">
- <tr><td>
- <font size="-1" face="helvetica, arial">
- last update at <!-- _GP_ when -->
- </font>
- </td></tr>
- </table>
- </td>
- </tr>
-
- </table>
- </body>
-</html>
