--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/Makefile Thu Dec 09 11:34:32 1999 +0100
@@ -0,0 +1,67 @@
+# --- uses $DISTNAME environment variable
+
+# --- perl scripts used in this makefile
+
+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 = ../../Distribution/doc/Contents
+
+# --- url prefixes for documentation links in main and dist dirs
+DIST_DOCU_PREFIX = $(DISTNAME)/doc/
+MAIN_DOCU_PREFIX = dist/$(DISTNAME)/doc/
+
+# --- target include files with documentation links
+DOC_CONTENTS_MAIN = docu-contents.main
+DOC_CONTENTS_DIST = docu-contents.dist
+
+# ---
+# --- begin rules
+
+all: clean gen
+
+gen: main dist
+
+main: check
+ $(MKCONTENT) -p $(MAIN_DOCU_PREFIX) $(DOC_CONTENT_FILE) $(DOC_CONTENTS_MAIN)
+ $(GENPAGE) -t $(MAIN_LAYOUT)/$(TEMPLATE_NAME) -c $(MAIN_CONTENT) -o $(MAIN_TARGET)
+
+ cd $(MAIN_TARGET); perl -pi -e "s/{ISABELLE}/$(DISTNAME)/g;" *.html
+
+dist: check
+ $(MKCONTENT) -p $(DIST_DOCU_PREFIX) $(DOC_CONTENT_FILE) $(DOC_CONTENTS_DIST)
+ $(GENPAGE) -t $(DIST_LAYOUT)/$(TEMPLATE_NAME) -c $(DIST_CONTENT) -o $(DIST_TARGET)
+
+ cd $(DIST_TARGET); perl -pi -e "s/{ISABELLE}/$(DISTNAME)/g;" *.html
+
+clean:
+ rm -rf $(MAIN_TARGET)
+ rm -rf $(DIST_TARGET)
+ rm -rf $(DOC_CONTENTS_MAIN)
+ rm -rf $(DOC_CONTENTS_DIST)
+ rm -f `find . -name "*~" -type f`
+
+check:
+ @if [ "$(DISTNAME)" = "" ]; then echo "Error: \$$DISTNAME not set."; exit 1; fi
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/bin/genpage Thu Dec 09 11:34:32 1999 +0100
@@ -0,0 +1,423 @@
+#!/bin/sh
+exec perl -x. $0 ${1+"$@"}
+#
+#!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;
+}
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/bin/mkcontents Thu Dec 09 11:34:32 1999 +0100
@@ -0,0 +1,47 @@
+#!/usr/bin/perl
+
+# mkcontents.pl
+# 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];
+
+$fileHeader = "<ul>\n";
+$lineHeader = " <li> ";
+$lineEnd = " </li>\n";
+$fileFooter = "</ul>\n";
+
+open(IN, "<$infile") || die "cannot read input file <$infile>";
+open(OUT, ">$outfile") || die "cannot write output file <$outfile>";
+
+print OUT $fileHeader;
+
+while (<IN>) {
+ if (/[ \t]*([^ \t]+)[ \t]+(.+)\n/) {
+ print OUT $lineHeader;
+ print OUT "<a href=\"$path$1.pdf\">$2</a>";
+ print OUT $lineEnd;
+ }
+}
+
+print OUT $fileFooter;
+
+close(OUT);
+close(IN);
+
+exit(0);
Binary file Admin/page/cambridge.gif has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/common/functions.pl Thu Dec 09 11:34:32 1999 +0100
@@ -0,0 +1,135 @@
+<!-- _GP_
+# undef all the functions we're defining. This stops lots of
+# complaining about re-defining the sub for each content file thats
+# processed.
+
+ if (defined(&me)) { undef &me; }
+ 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(&download)) { undef &download; }
+
+ -->
+
+<!-- _GP_
+
+ 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 "$month/$day/$year";
+# 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="100%" border="0" cellspacing="0" cellpadding="5">
+ <tr>
+ <td align=center bgcolor="$navcolor">
+ <b><font face="Arial,Helvetica"><A HREF="$_[1].html" target="_top">$_[0]</A></font></b>
+ </td>
+ </tr>
+ </table>
+EOF
+ }
+ else {
+ $retval = <<EOF;
+ <table width="100%" border="0" cellspacing="0" cellpadding="5">
+ <tr>
+ <td width="8"> </td>
+ <td width="150" 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;
+ <p>
+EOF
+ return $retval;
+ }
+
+ # size(filename)
+ sub size {
+ my $filename = $_[0];
+ my @s = stat $filename;
+ my $size = $s[7]/1024;
+
+ return sprintf("%.1f",$size);
+ }
+
+ sub setdowncolor {
+ $downcolor = $_[0];
+ return "";
+ }
+
+ # download(description, url, size)
+ sub download {
+
+ my $descr = $_[0];
+ my $url = $_[1];
+ my $size = $_[2];
+
+ if ($size eq "") {
+ $size = size($url);
+ $size = "$size K";
+ }
+
+ my $filename = $path;
+
+ if ($url =~ /([^\/]*\/)*([^\/]+)/) {
+ $filename = $2;
+ }
+
+ my $td = "nowrap bgcolor=$downcolor";
+
+ my $retval = <<EOF;
+ <tr>
+ <td align="left" $td>
+ $descr
+ </td>
+ <td align="left" $td>
+ <A HREF="$url">$filename</A>
+ </td>
+ <td align="right" $td>
+ $size
+ </td>
+ </tr>
+EOF
+
+ return $retval;
+ }
+
+ -->
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/dist-content/binary.content Thu Dec 09 11:34:32 1999 +0100
@@ -0,0 +1,32 @@
+%title%
+Isabelle Binary Distribution
+
+%body%
+The binary distribution of {ISABELLE} for rpm-based Linux/x86 systems:
+
+<p>
+
+<!-- _GP_ setdowncolor("#E0E0E0") -->
+<center>
+<table border="0" cellspacing="5" cellpadding="4" width="520">
+
+ <!-- _GP_ download("ML system", "rpm/smlnj-base-110.0.6-0.i386.rpm", "{RPM_SML_SIZE} K") -->
+ <!-- _GP_ download("Isabelle system", "rpm/isabelle.rpm", "{RPM_BASE_SIZE} K") -->
+ <!-- _GP_ download("Isabelle/HOL image", "rpm/isabelle-HOL.i386.rpm", "{RPM_HOL_SIZE} K") -->
+ <!-- _GP_ download("Isabelle/HOL-Real image (optional)", "rpm/isabelle-HOL-Real.i386.rpm", "{RPM_REAL_SIZE} K") -->
+ <!-- _GP_ download("Isabelle/ZF image (optional)", "rpm/isabelle-ZF.i386.rpm", "{RPM_ZF_SIZE} K") -->
+ <!-- _GP_ download("Isabelle pdf documentation (optional)", "rpm/isabelle-pdfdocs.rpm", "{RPM_DOCS_SIZE} K") -->
+
+</table>
+
+</center>
+
+<p>
+
+Example installation procedure:
+
+<pre>
+rpm -i smlnj-base-110.0.6-0.i386.rpm
+rpm -i --prefix /usr/share isabelle.rpm
+rpm -i --prefix /usr/share isabelle-HOL.i386.rpm
+</pre>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/dist-content/docs.content Thu Dec 09 11:34:32 1999 +0100
@@ -0,0 +1,9 @@
+%title%
+Isabelle Documentation
+
+%body%
+The Isabelle documentation:
+
+<!-- _GP_ include("$pwd/docu-contents.dist") -->
+
+All this documentation is also part of the Isabelle <a href="source.html">distribution</a>.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/dist-content/index.content Thu Dec 09 11:34:32 1999 +0100
@@ -0,0 +1,24 @@
+
+<!-- $Id$ -->
+
+%title%
+Isabelle Distribution Area
+
+
+%body%
+<p>
+
+<h2>Mirror sites (in alphabetical order)</h2>
+
+<ul>
+
+<li> <a href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/dist/">Cambridge (UK)</a> <br> </li>
+
+<li> <a href="http://isabelle.in.tum.de/dist/">Munich (Germany)</a> <br> </li>
+
+
+<li> <a href="ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html">New Jersey (USA)</a> <br> </li>
+
+</ul>
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/dist-content/past.content Thu Dec 09 11:34:32 1999 +0100
@@ -0,0 +1,17 @@
+%title%
+Isabelle Past Releases
+
+%body%
+<p>
+
+The past releases of Isabelle from the Cambrige ftp archive:
+
+<ul>
+<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle98-1.tar.gz">Isabelle98-1</a> </li>
+<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle98.tar.gz">Isabelle98</a> </li>
+<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-8.tar.gz">Isabelle94-8</a> </li>
+<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-7.tar.gz">Isabelle94-7</a> </li>
+<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94-6.tar.gz">Isabelle94-6</a> </li>
+<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle94.tar.gz">Isabelle94</a> </li>
+<li> <a href="ftp://ftp.cl.cam.ac.uk/ml/Isabelle93.tar.gz">Isabelle93</a> </li>
+</ul>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/dist-content/source.content Thu Dec 09 11:34:32 1999 +0100
@@ -0,0 +1,24 @@
+%title%
+Isabelle Source Releases
+
+%body%
+The source distribution of Isabelle:
+
+<p>
+
+<!-- _GP_ setdowncolor("#E0E0E0") -->
+
+<center>
+<table border="0" cellspacing="5" cellpadding="4" width="500">
+
+ <!-- _GP_ download("Isabelle sources with dvi documentation", "{ISABELLE}.tar.gz", "{PACKED_SIZE} K") -->
+ <!-- _GP_ download("Documentation as pdf files", "{ISABELLE}_pdf.tar.gz", "{PACKED_SIZE_PDF} K") -->
+ <!-- _GP_ download("All files unpacked", "{ISABELLE}", "{UNPACKED_SIZE} K") -->
+
+</table>
+</center>
+
+<p>
+
+Please see the Isabelle <a href="{ISABELLE}/README.html">README</a> file for more information.
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/dist-layout/navigation.html Thu Dec 09 11:34:32 1999 +0100
@@ -0,0 +1,27 @@
+<p>
+
+<center>
+<a href="index.html"><img src="{ISABELLE}/lib/logo/isabelle.gif"
+width="100" height="86" alt="[Isabelle logo]" border="0"></a>
+</center>
+<p>
+<center>
+<strong>Isabelle Distribution Area</strong>
+</center>
+
+<p>
+<!-- _GP_ setnavcolor("#F0F0F0") -->
+<!-- _GP_ page("Mirrors", "index") -->
+<!-- _GP_ empty_line(3) -->
+<!-- _GP_ page("Sources", "source") -->
+<!-- _GP_ empty_line(3) -->
+<!-- _GP_ page("Binaries", "binary") -->
+<!-- _GP_ empty_line(3) -->
+<!-- _GP_ page("Documentation", "docs") -->
+<!-- _GP_ empty_line(3) -->
+<!-- _GP_ page("Past Releases", "past") -->
+<!-- _GP_ empty_line(3) -->
+<!-- _GP_ empty_line(3) -->
+<!-- _GP_ empty_line(3) -->
+
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/dist-layout/template.html Thu Dec 09 11:34:32 1999 +0100
@@ -0,0 +1,67 @@
+<!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">
+ <!-- _GP_ content("meta") -->
+ <script language="JavaScript">
+ <!--
+ if( top.parent.frames.length > 0)
+ top.parent.location.href = self.location.href;
+ // -->
+ </script>
+ </head>
+
+ <body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040">
+
+ <table border="0" cellspacing="5" width="100%" height="100%">
+
+ <tr>
+ <td width="20%" valign="top" bgcolor="#D8D8FF">
+ <!-- _GP_ include("$pwd/dist-layout/navigation.html") -->
+ </td>
+
+ <td width="80%" valign="top">
+
+ <center>
+ <table width="70%" border="0" cellspacing="10" cellpadding="10">
+ <tr>
+ <td align="center" bgcolor="#D8D8FF">
+ <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>
--- a/Admin/page/index.html Wed Dec 08 13:53:29 1999 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,164 +0,0 @@
-<html>
-
-<head>
-<!-- $Id$ -->
-<title>Isabelle</title>
-</head>
-
-<body>
-
-<h1>Isabelle </h1> <a href="http://isabelle.in.tum.de/logo/"><img
-src="isabelle.gif" width=100 align=right alt="[Isabelle logo]"></a>
-
-<p>
-
-<strong>Isabelle</strong> 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>).
-
-<p>
-
-<a
-href="http://www.cl.cam.ac.uk/Research/HVG/Isabelle/cambridge.html"><img
-src="cambridge.gif" width=145 border=0 align=right
-alt="[Cambridge logo]"></a> <a
-href="http://isabelle.in.tum.de/munich.html"><img src="munich.gif"
-width=48 border=0 align=right alt="[Munich logo]"></a> This page
-provides 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://isabelle.in.tum.de/munich.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.
-
-
-<h2>Obtaining Isabelle</h2>
-
-The current version is <strong>Isabelle99</strong>. Several mirror
-sites provide the Isabelle <a href="dist/">distribution</a>, which
-includes sources, documentation, and binary packages.
-
-
-<h2>What is Isabelle?</h2>
-
-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.
-
-
-<h3>Isabelle's Logics</h3>
-
-The Isabelle distribution includes a large body of object logics and
-other examples (see the <a href="library/">Isabelle theory
-library</a>).
-
-<dl>
-
-<dt><a href="library/HOL/"><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.html">HOL
-System</A>.
-
-<dt><a href="library/HOLCF/"><strong>Isabelle/HOLCF</strong></a><dd>
-adds Scott's Logic for Computable Functions (domain theory) to HOL.
-
-<dt><a href="library/FOL/"><strong>Isabelle/FOL</strong></a><dd>
-provides basic classical and intuitionistic first-order logic. It is
-polymorphic.
-
-<dt><a href="library/ZF/"><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/">HOL/Auth</a>) or
-communication protocols (<a href="library/HOLCF/IOA/">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/">CTT</a> is an extensional version of
-Martin-Löf's Type Theory, <a href="library/Cube/">Cube</a> is
-Barendregt's Lambda Cube. There are also some sequent calculus
-examples under <a href="library/Sequents/">Sequents</a>, including
-modal and linear logics. Again see the <a href="library/">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).
-
-
-<h2>Mailing list</h2>
-
-Use the mailing list <a href="mailto:
-isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a> to
-discuss problems and results.
-(Why not <A HREF="mailto:lcp@cl.cam.ac.uk">subscribe</A>?)
-
-
-</body>
-
-</html>
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/main-content/about.content Thu Dec 09 11:34:32 1999 +0100
@@ -0,0 +1,102 @@
+%title%
+About Isabelle
+
+%body%
+<h2>What is Isabelle?</h2>
+
+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.
+
+
+<h3>Isabelle's Logics</h3>
+
+The Isabelle distribution includes a large body of object logics and
+other examples (see the <a href="library/">Isabelle theory
+library</a>).
+
+<dl>
+
+<dt><a href="library/HOL/"><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.html">HOL
+System</A>.
+
+<dt><a href="library/HOLCF/"><strong>Isabelle/HOLCF</strong></a><dd>
+adds Scott's Logic for Computable Functions (domain theory) to HOL.
+
+<dt><a href="library/FOL/"><strong>Isabelle/FOL</strong></a><dd>
+provides basic classical and intuitionistic first-order logic. It is
+polymorphic.
+
+<dt><a href="library/ZF/"><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/">HOL/Auth</a>) or
+communication protocols (<a href="library/HOLCF/IOA/">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/">CTT</a> is an extensional version of
+Martin-Löf's Type Theory, <a href="library/Cube/">Cube</a> is
+Barendregt's Lambda Cube. There are also some sequent calculus
+examples under <a href="library/Sequents/">Sequents</a>, including
+modal and linear logics. Again see the <a href="library/">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/cambridge.gif has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/main-content/docs.content Thu Dec 09 11:34:32 1999 +0100
@@ -0,0 +1,8 @@
+%title%
+Isabelle Documentation
+
+%body%
+
+<!-- _GP_ include("$pwd/docu-contents.main") -->
+
+All this documentation is also part of the Isabelle <a href="dist/">distribution</a>.
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/main-content/index.content Thu Dec 09 11:34:32 1999 +0100
@@ -0,0 +1,53 @@
+%title%
+Isabelle
+
+%body%
+
+<p>
+
+<h2>Isabelle</h2>
+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>).
+
+<p>
+
+This page provides 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="munich.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>Obtaining Isabelle</h2>
+
+The current version is <strong>{ISABELLE}</strong>. Several mirror
+sites provide the Isabelle <a href="dist/">distribution</a>, which
+includes sources, documentation, and binary packages.
+
+
+<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> to
+discuss problems and results.
+(Why not <A HREF="mailto:lcp@cl.cam.ac.uk">subscribe</A>?)
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/main-content/munich.content Thu Dec 09 11:34:32 1999 +0100
@@ -0,0 +1,76 @@
+%title%
+Isabelle at Munich
+
+
+%body%
+
+<h1>Isabelle at Munich</h1>
+
+<p>
+
+<a href="http://isabelle.in.tum.de/">Isabelle</a> is a 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>).
+This is the local page of the Munich group.
+
+
+<h2>People</h2>
+
+The following people are involved in Isabelle applications or
+development at our group (alphabetical order):
+
+<ul>
+
+<li> <a href="http://www.in.tum.de/~bauerg/">Gertrud Bauer</a>
+<li> <a href="/~berghofe/">Stefan Berghofer</a>
+<li> <a href="/~kleing/">Gerwin Klein</a>
+<li> <a href="/~narasche/">Wolfgang Naraschewski</a>
+<li> <a href="/~nipkow/">Tobias Nipkow</a>
+<li> <a href="/~oheimb/">David von Oheimb</a>
+<li> <a href="/~prensani/">Leonor Prensa Nieto</a>
+<li> <a href="/~pusch/">Cornelia Pusch</a>
+<li> <a href="/~wenzelm/">Markus Wenzel</a>
+
+</ul>
+
+
+<h2>Projects</h2>
+
+The main Isabelle related projects at TU Munich are currently:
+
+<ul>
+
+<li> <b><a href="Bali/">Isabelle/Bali</a></b> Java and JVM
+formalization --- type system, semantics, compilers
+
+<li> <b>Isabelle/HOOL</b> Object-oriented verification of Java
+programs
+
+<li> <b><a href="Isar/">Isabelle/Isar</a></b> Intelligible
+semi-automated reasoning --- readable formal proof documents
+
+<li><b><a href="IOA/">Isabelle/IOA</a></b> Verification of
+distributed, reactive systems using I/O Automata
+
+</ul>
+
+<p>
+
+<b>Important local information:</b> Students are welcome to
+participate, see <a href="stud/">Isabelle Projekte für Studenten</a>
+(in German) for more information.
+
+
+<h2>Isabelle resources</h2>
+
+<ul>
+
+<li> Isabelle <a href="dist/">distribution area</a>
+
+<li> Isabelle online theory library: <a
+href="library-Isabelle99/">Isabelle99</a>, <a
+href="library-Isabelle98-1/">Isabelle98-1</a>
+
+
+</ul>
Binary file Admin/page/main-content/munich.gif has changed
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/main-layout/navigation.html Thu Dec 09 11:34:32 1999 +0100
@@ -0,0 +1,19 @@
+<p>
+
+<center>
+<a href="index.html"><img src="dist/{ISABELLE}/lib/logo/isabelle.gif" width="100" height="86" alt="[Isabelle logo]" border="0"></a>
+</center>
+<p>
+
+<p>
+<!-- _GP_ setnavcolor("#F0F0F0") -->
+<!-- _GP_ page("Home", "index") -->
+<!-- _GP_ empty_line(3) -->
+<!-- _GP_ page("About", "about") -->
+<!-- _GP_ empty_line(3) -->
+<!-- _GP_ page("Documentation", "docs") -->
+<!-- _GP_ empty_line(3) -->
+<!-- _GP_ page("Download", "dist/index") -->
+<!-- _GP_ empty_line(3) -->
+<!-- _GP_ empty_line(3) -->
+
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/Admin/page/main-layout/template.html Thu Dec 09 11:34:32 1999 +0100
@@ -0,0 +1,74 @@
+<!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">
+ <!-- _GP_ content("meta") -->
+ <script language="JavaScript">
+ <!--
+ if( top.parent.frames.length > 0)
+ top.parent.location.href = self.location.href;
+ // -->
+ </script>
+ </head>
+
+ <body text="#000000" bgcolor="#FFFFFF" link="#0000FF" vlink="#000099" alink="#404040">
+
+ <table border="0" cellspacing="5" width="100%" height="100%">
+
+ <tr>
+ <td width="20%" valign="top" bgcolor="#aacccc">
+ <!-- _GP_ include("$pwd/main-layout/navigation.html") -->
+ </td>
+
+ <td width="80%" valign="top">
+
+ <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://isabelle.in.tum.de/munich.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>
+ </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/munich.gif has changed
