<!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") -->
</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="#aacccc">
<!-- _GP_ include("$pwd/main-layout/navigation.html") -->
<table height="20"><tr><td> </td></tr></table>
</td>
<td width="100%" 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://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>
</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>