# HG changeset patch
# User kleing
# Date 944735672 -3600
# Node ID 3c587e7b8fe51aef75321b4d9e400b26330a63a8
# Parent  bb15396278fb6404ad0e4a05de27df5f884f8496
new webpage layout

diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/Makefile
--- /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
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/bin/genpage
--- /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;
+}
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/bin/mkcontents
--- /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);
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/cambridge.gif
Binary file Admin/page/cambridge.gif has changed
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/common/functions.pl
--- /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">&nbsp;</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">&nbsp;</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>
+          &nbsp; $descr
+        </td>
+        <td align="left" $td>
+          &nbsp; <A HREF="$url">$filename</A>
+        </td>
+        <td align="right" $td>
+          &nbsp; $size &nbsp;
+        </td>
+      </tr>
+EOF
+
+      return $retval;
+    }
+
+ -->
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/dist-content/binary.content
--- /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>
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/dist-content/docs.content
--- /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>.
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/dist-content/index.content
--- /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>&nbsp;</li>
+
+<li> <a href="http://isabelle.in.tum.de/dist/">Munich (Germany)</a> <br>&nbsp;</li>
+	
+
+<li> <a href="ftp://ftp.research.bell-labs.com/dist/smlnj/isabelle/index.html">New Jersey (USA)</a> <br>&nbsp;</li>
+
+</ul>
+
+
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/dist-content/past.content
--- /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>
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/dist-content/source.content
--- /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.
+
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/dist-layout/navigation.html
--- /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>
+&nbsp;
+<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>
+&nbsp;
+<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) -->
+&nbsp;
+&nbsp;
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/dist-layout/template.html
--- /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>
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/index.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&ouml;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>
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/main-content/about.content
--- /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&ouml;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).
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/main-content/cambridge.gif
Binary file Admin/page/main-content/cambridge.gif has changed
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/main-content/docs.content
--- /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>.
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/main-content/index.content
--- /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>
+&nbsp;
+
+<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>
+&nbsp;
+
+
+<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>?)
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/main-content/munich.content
--- /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>
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/main-content/munich.gif
Binary file Admin/page/main-content/munich.gif has changed
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/main-layout/navigation.html
--- /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>
+&nbsp;
+<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>
+&nbsp;
+<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) -->
+&nbsp;
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/main-layout/template.html
--- /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>
diff -r bb15396278fb -r 3c587e7b8fe5 Admin/page/munich.gif
Binary file Admin/page/munich.gif has changed