Commit [69143c] default tip Maximize Restore History

close in-repos Isabelle2003 branch

gerwin.klein@nicta.com.au gerwin.klein@nicta.com.au 2009-09-17

1 2 3 > >> (Page 1 of 3)
added admin/main-config
added admin/mail-attach
added admin/cvs-sync
added admin/report.pl
added web/entries/nav.html
added web/submit-template
added web/nav.html
added web/search.shtml
changed admin/testall
changed admin/publish
changed web/front.css
copied web/entries/Submission-Template.html -> web/entries/Functional-Automata.shtml
copied web/entries/Example-Submission.html -> web/entries/MiniML.shtml
copied web/download.html -> web/entries/Example-Submission.shtml
copied web/search.html -> web/entries/AVL-Trees.shtml
copied web/index.html -> web/entries/Submission-Template.shtml
copied web/about.html -> web/about.shtml
copied web/submitting.html -> admin/regression
admin/main-config Diff Switch to side-by-side view
Loading...
admin/mail-attach Diff Switch to side-by-side view
Loading...
admin/cvs-sync Diff Switch to side-by-side view
Loading...
admin/report.pl Diff Switch to side-by-side view
Loading...
web/entries/nav.html Diff Switch to side-by-side view
Loading...
web/submit-template Diff Switch to side-by-side view
Loading...
web/nav.html Diff Switch to side-by-side view
Loading...
web/search.shtml Diff Switch to side-by-side view
Loading...
admin/testall Diff Switch to side-by-side view
Loading...
admin/publish Diff Switch to side-by-side view
Loading...
web/front.css Diff Switch to side-by-side view
Loading...
web/entries/Submission-Template.html to web/entries/Functional-Automata.shtml
--- a/web/entries/Submission-Template.html
+++ b/web/entries/Functional-Automata.shtml
@@ -14,30 +14,7 @@
     <tr>
       <td width="20%" align="center" valign="top">
       <!-- navigation -->
-
-	  <p>&nbsp;</p>
-
-	  <a href="http://isabelle.in.tum.de"><img src="../images/isabelle.png" 
-width="100" height="86" border=0></a>
-	  <p>&nbsp;</p>
-	  <p>&nbsp;</p>
-
-	  <table class="nav">
-      <tr><td class="nav" width="100%"><a href="../index.html">Home</a> 
-</td></tr>      <tr><td class="nav"><a href="../about.html">About</a> </td></tr>
-      <tr><td class="nav"><a href="../submitting.html">Submission Guidelines</a> 
-</td></tr>      <tr><td class="nav"><a href="../search.html">Search</a> 
-</td></tr>      <tr><td class="nav"><a href="../download.html">Download</a> 
-</td></tr>      </table>
-
-	  <p>&nbsp;</p>
-	  <p>&nbsp;</p>
-	<a
-    href="http://sourceforge.net"><img
-    src="http://sourceforge.net/sflogo.php?group_id=101909&amp;type=1"
-    width="88" height="31" border="0" alt="SourceForge.net Logo"
-    /></a>
-
+      <!--#include file="nav.html"-->
       </td>
       <td width="80%" valign="top">
       <!-- content -->
@@ -46,58 +23,73 @@
 <p>&nbsp;</p>
 
 <!-- begin entry data: -->
-<h1><!-- Title: -->???</h1>
+<h1><!-- Title: -->Functional Automata</h1>
 <p>&nbsp;</p>
 
 <table width="80%" class="data">
   <tbody>
     <tr><td class="datahead" width="20%">Title:</td>
     <td class="data" width="80%">
-<!-- Title: -->???
+<!-- Title: -->Functional Automata
     </td></tr>
 		
     <tr><td class="datahead">Author:</td>
 <td class="data">
 <!-- Author: --><a
-href="???">???</a>
+href="http://www.in.tum.de/~nipkow/">Tobias Nipkow</a>
 </td></tr>		
     
 	<tr><td class="datahead">Submisison date:</td>
 	
-<td class="data"><!-- Submission date: -->????-??-??</td></tr>
+<td class="data"><!-- Submission date: -->2004-03-30</td></tr>
 
 	<tr><td class="datahead" valign="top">Abstract:</td>
   <td class="abstract"> 
 <!-- Abstract: -->	
-???
-
+This theory defines deterministic and nondeterministic automata in a
+functional representation: the transition function/relation and the finality
+predicate are just functions. Hence the state space may be infinite.  It is
+shown how to convert regular expressions into such automata. A scanner
+(generator) is implemented with the help of functional automata: the scanner
+chops the input up into longest recognized substrings. Finally we also show
+how to convert a certain subclass of functional automata (essentially the
+finite deterministic ones) into regular sets.
    </td></tr>
 </tbody>
 </table>
 
 <p>&nbsp;</p>
 
+<!-- entry directory name: -->
+<!--#set var="name" value="Functional-Automata" -->
+
+<!--#set var="doc" value="../browser_info/current/HOL/${name}/document.pdf" -->
+<!--#set var="browse" value="../browser_info/current/HOL/${name}/index.html" -->
+<!--#set var="tar" value="../release/afp-${name}-current.tar.gz" -->
+
 <table class="links">
   <tbody>
-    <tr><td class="links">	
-<!-- link to document, only needs session name changed -->	
-<!-- link to README.hmtl if no document exists -->	
-<a href="../browser_info/current/HOL/???/document.pdf">Proof document</a>	
+    <tr>
+  <td class="links">
+	<a href="<!--#echo var="doc" -->">Proof document</a>
+  </td>
+	<!-- link to README.hmtl if no document exists -->	
+	</tr>
+    <tr>
+  <td class="links">
+	<a href="<!--#echo var="browse" -->">Browse theories</a>
 	</td></tr>
-    <tr><td class="links">
-<!-- link to browser info, only needs session name changed: -->
-<a href="../browser_info/current/HOL/???/index.html">Browse theories</a>
-    </td></tr>
-    <tr><td class="links"> 	
-<!-- link to tar gz, only needs session name changed: -->	
-<a href="../release/afp-???-current.tar.gz">Download this entry</a>	</td></tr>
-
+    <tr>
+  <td class="links"> 
+	<a href="<!--#echo var="tar" -->">Download this entry</a>
+	</td>
+  </tr>
     <tr><td class="links">Older releases:	None</td></tr>
   </tbody>
 </table>
-<!-- end entry data -->
+<!-- entry data end -->
 
 </td> </tr> </table>
-<div align="right" class="date">$Date: 2004-02-25 02:37:14 $, $Revision: 1.1 
+<div align="right" class="date">$Date: 2004-03-30 10:09:13 $, $Revision: 1.1 
 $</div></body>
 </html>
web/entries/Example-Submission.html to web/entries/MiniML.shtml
--- a/web/entries/Example-Submission.html
+++ b/web/entries/MiniML.shtml
@@ -14,81 +14,78 @@
     <tr>
       <td width="20%" align="center" valign="top">
       <!-- navigation -->
-
-	  <p> </p>
-
-	  <a href="http://isabelle.in.tum.de"><img src="../images/isabelle.png" width="100" height="86" border=0></a>
-
-	  <p> </p>
-	  <p> </p>
-
-	  <table class="nav">
-      <tr><td class="nav" width="100%"><a href="../index.html">Home</a> </td></tr>
-      <tr><td class="nav"><a href="../about.html">About</a> </td></tr>
-      <tr><td class="nav"><a href="../submitting.html">Submission Guidelines</a> </td></tr>
-      <tr><td class="nav"><a href="../search.html">Search</a> </td></tr>
-      <tr><td class="nav"><a href="../download.html">Download</a> </td></tr>
-      </table>
-
-	  <p> </p>
-	  <p> </p>
-	<a
-    href="http://sourceforge.net"><img
-    src="http://sourceforge.net/sflogo.php?group_id=101909&amp;type=1"
-    width="88" height="31" border="0" alt="SourceForge.net Logo"
-    /></a>
-
+      <!--#include file="nav.html"-->
       </td>
       <td width="80%" valign="top">
       <!-- content -->
 
 <div align="center">
-<p> </p>
-<!-- entry data here: -->
-<h1><font class="first">E</font>xample 
-    <font class="first">S</font>ubmission</h1>
-<p> </p>
+<p>&nbsp;</p>
+
+<!-- begin entry data: -->
+<h1><!-- Title: -->Mini ML</h1>
+<p>&nbsp;</p>
 
 <table width="80%" class="data">
   <tbody>
     <tr><td class="datahead" width="20%">Title:</td>
-	    <td class="data" width="80%">Example Submission</td></tr>
+    <td class="data" width="80%">
+<!-- Title: -->Mini ML
+    </td></tr>
 		
     <tr><td class="datahead">Author:</td>
-	    <td class="data"><a href="http://www.cse.unsw.edu.au/~kleing">Gerwin Klein</a></td></tr>
-		
-    <tr><td class="datahead">Submisison date:</td> 
-	    <td class="data">2003-02-25</td></tr>
-		
+<td class="data">
+<!-- Author: -->
+Wolfgang Naraschewski and <a href="http://www4.in.tum.de/~nipkow/">Tobias Nipkow</a>
+</td></tr>		
+    
+	<tr><td class="datahead">Submisison date:</td>
+	
+<td class="data"><!-- Submission date: -->2004-03-19</td></tr>
+
 	<tr><td class="datahead" valign="top">Abstract:</td>
-	    <td class="abstract">   
-This is an example submission to the Archive of Formal Proof. It shows
-submission requirements and explains the structure of a simple typical
-submission.
+  <td class="abstract"> 
+<!-- Abstract: -->	
+This theory defines the type inference rules and the type inference algorithm
+<em>W</em> for MiniML (simply-typed lambda terms with <tt>let</tt>) due to
+Milner. It proves the soundness and completeness of <em>W</em> w.r.t. the
+rules.
    </td></tr>
 </tbody>
 </table>
 
-<p> </p>
+<p>&nbsp;</p>
+
+<!-- entry directory name: -->
+<!--#set var="name" value="MiniML" -->
+
+<!--#set var="doc" value="../browser_info/current/HOL/${name}/document.pdf" -->
+<!--#set var="browse" value="../browser_info/current/HOL/${name}/index.html" -->
+<!--#set var="tar" value="../release/afp-${name}-current.tar.gz" -->
 
 <table class="links">
   <tbody>
-    <tr><td class="links">
-	<a href="../browser_info/current/HOL/Example-Submission/document.pdf">Proof document</a>
+    <tr>
+  <td class="links">
+	<a href="<!--#echo var="doc" -->">Proof document</a>
+  </td>
 	<!-- link to README.hmtl if no document exists -->	
+	</tr>
+    <tr>
+  <td class="links">
+	<a href="<!--#echo var="browse" -->">Browse theories</a>
 	</td></tr>
-    <tr><td class="links">
-	<a href="../browser_info/current/HOL/Example-Submission/index.html">Browse theories</a>
-	</td></tr>
-    <tr><td class="links"> 
-	<a href="../release/afp-Example-Submission-current.tar.gz">Download this entry</a>
-	</td></tr>
+    <tr>
+  <td class="links"> 
+	<a href="<!--#echo var="tar" -->">Download this entry</a>
+	</td>
+  </tr>
     <tr><td class="links">Older releases:	None</td></tr>
   </tbody>
 </table>
 <!-- entry data end -->
 
 </td> </tr> </table>
-<div align="right" class="date">$Date: 2004-02-25 02:37:14 $, $Revision: 1.1 $</div>
-</body>
+<div align="right" class="date">$Date: 2004-03-23 06:23:47 $, $Revision: 1.1 
+$</div></body>
 </html>
web/download.html to web/entries/Example-Submission.shtml
--- a/web/download.html
+++ b/web/entries/Example-Submission.shtml
@@ -2,82 +2,81 @@
 		"http://www.w3.org/TR/html4/loose.dtd">
 <html>
 <head>
-<title>The Archive of Formal Proofs</title>
-<link rel="stylesheet" type="text/css" href="front.css">
-<meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
-<meta name="GENERATOR" content="Quanta Plus">
+  <title>Archive of Formal Proofs</title>
+  <link rel="stylesheet" type="text/css" href="front.css">
+  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
+  <meta name="GENERATOR" content="Quanta Plus">
 </head>
 <body>
 
 <table width="100%">
-<tbody>
-	<tr>
-	<td width="20%" align="center" valign="top">
-	<!-- navigation -->
-
-	<p>&nbsp;</p>
-
-	<a href="http://isabelle.in.tum.de"><img src="images/isabelle.png"
-width="100" height="86" border=0></a>
-	<p>&nbsp;</p>
-	<p>&nbsp;</p>
-
-	<table class="nav">
-	<tr><td class="nav" width="100%"><a href="index.html">Home</a> </td></tr>
-	<tr><td class="nav"><a href="about.html">About</a> </td></tr>
-	<tr><td class="nav"><a href="submitting.html">Submission Guidelines</a>
-</td></tr>      <tr><td class="nav"><a href="search.html">Search</a> </td></tr>
-	<tr><td class="nav"><a href="download.html">Download</a> </td></tr>
-	</table>
-
-	<p>&nbsp;</p>
-	<p>&nbsp;</p>
-	<a
-	href="http://sourceforge.net"><img
-	src="http://sourceforge.net/sflogo.php?group_id=101909&amp;type=1"
-	width="88" height="31" border="0" alt="SourceForge.net Logo"
-	/></a>
-
-	</td>
-	<td width="80%" valign="top">
-	<!-- content -->
+  <tbody>
+    <tr>
+      <td width="20%" align="center" valign="top">
+      <!-- navigation -->
+      <!--#include file="nav.html"-->
+      </td>
+      <td width="80%" valign="top">
+      <!-- content -->
 
 <div align="center">
-<p>&nbsp;</p>
-<h1><font class="first">D</font>ownload the
-	<font class="first">A</font>rchive</h1>
-<p>&nbsp;</p>
+<p>�</p>
+<!-- entry data here: -->
+<h1><font class="first">E</font>xample 
+    <font class="first">S</font>ubmission</h1>
+<p>�</p>
 
-<p>&nbsp;</p>
+<table width="80%" class="data">
+  <tbody>
+    <tr><td class="datahead" width="20%">Title:</td>
+	    <td class="data" width="80%">Example Submission</td></tr>
+		
+    <tr><td class="datahead">Author:</td>
+	    <td class="data"><a href="http://www.cse.unsw.edu.au/~kleing/">Gerwin Klein</a></td></tr>
+		
+    <tr><td class="datahead">Submisison date:</td> 
+	    <td class="data">2003-02-25</td></tr>
+		
+	<tr><td class="datahead" valign="top">Abstract:</td>
+	    <td class="abstract">   
+This is an example submission to the Archive of Formal Proof. It shows
+submission requirements and explains the structure of a simple typical
+submission.
+   </td></tr>
+</tbody>
+</table>
 
-<table width="80%" class="descr">
-<tbody>
-	<tr><td class="head"><b>Current stable version</b> (for current Isabelle
-	release):</td></tr>
-		<tr></tr><td class="entry">&nbsp;&nbsp;<a
-			href="release/afp-current.tar.gz"><tt>afp-current.tar.gz</tt></a>
-                        <!--#flastmod file="index.html" -->
-                        </td></tr>
+<p>�</p>
 
-		<tr><td class="head">Older stable versions:</td></tr>
-		<tr><td class="entry">Please use the <a
-	href="http://sourceforge.net/project/showfiles.php?group_id=101909">sourceforge
-	download system</a> to access older versions of the archive.</td></tr>
+<!--#set var="name" value="Example-Submission" -->
 
-	<tr><td class="head">Development snapshot (for development snapshot
-	of Isabelle):</td></tr>
+<!--#set var="doc" value="../browser_info/current/HOL/${name}/document.pdf" -->
+<!--#set var="browse" value="../browser_info/current/HOL/${name}/index.html" -->
+<!--#set var="tar" value="../release/afp-${name}-current.tar.gz" -->
 
-	<tr><td class="entry">&nbsp;&nbsp;<a
-			href="release/afp-devel.tar.gz"><tt>afp-devel.tar.gz</tt></a></td></tr></tr>
+<table class="links">
+  <tbody>
+    <tr>
+  <td class="links">
+	<a href="<!--#echo var="doc" -->">Proof document</a>
+  </td>
+	<!-- link to README.hmtl if no document exists -->	
+	</tr>
+    <tr>
+  <td class="links">
+	<a href="<!--#echo var="browse" -->">Browse theories</a>
+	</td></tr>
+    <tr>
+  <td class="links"> 
+	<a href="<!--#echo var="tar" -->">Download this entry</a>
+	</td>
+  </tr>
+    <tr><td class="links">Older releases:	None</td></tr>
+  </tbody>
+</table>
+<!-- entry data end -->
 
-	<tr><td class="head">CVS access:</td></tr>	
-
-	<tr><td class="entry">Please refer to 
-	the <a href="http://sourceforge.net/cvs/?group_id=101909">description</a> on 
-	sourceforge. Use <tt>thys</tt> as module name. You can also <a 
-	href="http://cvs.sourceforge.net/viewcvs.py/afp/">browse</a> the repository 
-	online </td></tr>
-
-	</tbody></table></td> </tr> </table>
+</td> </tr> </table>
+<div align="right" class="date">$Date: 2004-03-05 11:01:02 $, $Revision: 1.1.2.3 $</div>
 </body>
 </html>
web/search.html to web/entries/AVL-Trees.shtml
--- a/web/search.html
+++ b/web/entries/AVL-Trees.shtml
@@ -1,75 +1,90 @@
-<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN
-		"http://www.w3.org/TR/html4/loose.dtd"">
+<!DOCTYPE public "-//w3c//dtd html 4.01 transitional//en"
+		"http://www.w3.org/TR/html4/loose.dtd">
 <html>
 <head>
-  <title>Search the Archive of Formal Proofs</title>
+  <title>Archive of Formal Proofs</title>
   <link rel="stylesheet" type="text/css" href="front.css">
-  <meta http-equiv="Content-Type" content="text/html; charset=ISO-8859-1">
+  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   <meta name="GENERATOR" content="Quanta Plus">
 </head>
 <body>
-  <table width="100%">
+
+<table width="100%">
   <tbody>
     <tr>
       <td width="20%" align="center" valign="top">
       <!-- navigation -->
-
-	  <p>&nbsp;</p>
-
-	  <a href="http://isabelle.in.tum.de"><img src="images/isabelle.png" width="100" height="86" border=0></a>
-
-	  <p>&nbsp;</p>
-	  <p>&nbsp;</p>
-
-	  <table class="nav">
-      <tr><td class="nav" width="100%"><a href="index.html">Home</a> </td></tr>
-      <tr><td class="nav"><a href="about.html">About</a> </td></tr>
-      <tr><td class="nav"><a href="submitting.html">Submission Guidelines</a> </td></tr>
-      <tr><td class="nav"><a href="search.html">Search</a> </td></tr>
-      <tr><td class="nav"><a href="download.html">Download</a> </td></tr>
-      </table>
-
-	  <p>&nbsp;</p>
-	  <p>&nbsp;</p>
-	<a
-    href="http://sourceforge.net"><img
-    src="http://sourceforge.net/sflogo.php?group_id=101909&amp;type=1"
-    width="88" height="31" border="0" alt="SourceForge.net Logo"
-    /></a>
-
+      <!--#include file="nav.html"-->
       </td>
       <td width="80%" valign="top">
       <!-- content -->
 
 <div align="center">
-<p>&nbsp;</p>
-<h1><font class="first">S</font>earch the <font class="first">A</font>rchive</h1>
-<p>&nbsp;</p>
-<p>&nbsp;</p>
-<p>&nbsp;</p>
-<div align="center"><!-- SiteSearch Google -->
-<p>Use Google to search the archive. It will look in entry descriptions 
-as well as in the Isabelle theories and PDF proof documents.</p>
-<p>&nbsp;</p>
-<FORM method=GET action="http://www.google.com/search">
-<TABLE bgcolor="#FFFFFF"><tr><td>
-<A HREF="http://www.google.com/">
-<IMG SRC="http://www.google.com/logos/Logo_40wht.gif" 
-border="0" ALT="Google"></A>
-</td>
-<td>
-<INPUT TYPE=text name=q size=31 maxlength=255 value="">
-<INPUT type=submit name=btnG VALUE="Google Search">
-<font size=-1>
-<input type=hidden name=domains value="afp.sf.net"><br><input type=radio name=sitesearch value=""> Web <input type=radio name=sitesearch value="afp.sf.net" checked>Archive of Formal Proofs<br>
-</font>
-</td></tr></TABLE>
-</FORM>
-<!-- SiteSearch Google -->
-<p>&nbsp;</p>
-<p>Google indexes new pages every 6-8 weeks. Submissions newer than that might be missed.</p>
-</div>
+<p>�</p>
+
+<!-- begin entry data: -->
+<h1><!-- Title: -->AVL Trees</h1>
+<p>�</p>
+
+<table width="80%" class="data">
+  <tbody>
+    <tr><td class="datahead" width="20%">Title:</td>
+    <td class="data" width="80%">
+<!-- Title: -->AVL Trees
+    </td></tr>
+		
+    <tr><td class="datahead">Author:</td>
+<td class="data">
+<!-- Author: -->Cornelia Pusch and <a
+href="http://www4.in.tum.de/~nipkow/">Tobias Nipkow</a>
+</td></tr>		
+    
+	<tr><td class="datahead">Submisison date:</td>
+	
+<td class="data"><!-- Submission date: -->2004-03-19</td></tr>
+
+	<tr><td class="datahead" valign="top">Abstract:</td>
+  <td class="abstract"> 
+<!-- Abstract: -->	
+  A small demo formalization of AVL trees with room for improvement.
+  If you are interested in working on this, please contact 
+  <tt>gerwin.klein@nicta.com.au</tt>.
+   </td></tr>
+</tbody>
+</table>
+
+<p>�</p>
+
+<!-- entry directory name: -->
+<!--#set var="name" value="AVL-Trees" -->
+
+<!--#set var="doc" value="../browser_info/current/HOL/${name}/document.pdf" -->
+<!--#set var="browse" value="../browser_info/current/HOL/${name}/index.html" -->
+<!--#set var="tar" value="../release/afp-${name}-current.tar.gz" -->
+
+<table class="links">
+  <tbody>
+    <tr>
+  <td class="links">
+	<a href="<!--#echo var="doc" -->">Proof document</a>
+  </td>
+	<!-- link to README.hmtl if no document exists -->	
+	</tr>
+    <tr>
+  <td class="links">
+	<a href="<!--#echo var="browse" -->">Browse theories</a>
+	</td></tr>
+    <tr>
+  <td class="links"> 
+	<a href="<!--#echo var="tar" -->">Download this entry</a>
+	</td>
+  </tr>
+    <tr><td class="links">Older releases:	None</td></tr>
+  </tbody>
+</table>
+<!-- entry data end -->
 
 </td> </tr> </table>
-</body>
+<div align="right" class="date">$Date: 2004-03-19 00:01:02 $, $Revision: 1.1 
+$</div></body>
 </html>
web/index.html to web/entries/Submission-Template.shtml
--- a/web/index.html
+++ b/web/entries/Submission-Template.shtml
@@ -2,7 +2,7 @@
 		"http://www.w3.org/TR/html4/loose.dtd">
 <html>
 <head>
-  <title>The Archive of Formal Proofs</title>
+  <title>Archive of Formal Proofs</title>
   <link rel="stylesheet" type="text/css" href="front.css">
   <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
   <meta name="GENERATOR" content="Quanta Plus">
@@ -14,81 +14,76 @@
     <tr>
       <td width="20%" align="center" valign="top">
       <!-- navigation -->
-
-	  <p>&nbsp;</p>
-
-	  <a href="http://isabelle.in.tum.de"><img src="images/isabelle.png" 
-width="100" height="86" border=0></a>
-	  <p>&nbsp;</p>
-	  <p>&nbsp;</p>
-
-	  <table class="nav">
-      <tr><td class="nav" width="100%"><a href="index.html">Home</a> </td></tr>
-      <tr><td class="nav"><a href="about.html">About</a> </td></tr>
-      <tr><td class="nav"><a href="submitting.html">Submission Guidelines</a> 
-</td></tr>      <tr><td class="nav"><a href="search.html">Search</a> </td></tr>
-      <tr><td class="nav"><a href="download.html">Download</a> </td></tr>
-      </table>
-
-	  <p>&nbsp;</p>
-	  <p>&nbsp;</p>
-	<a
-    href="http://sourceforge.net"><img
-    src="http://sourceforge.net/sflogo.php?group_id=101909&amp;type=1"
-    width="88" height="31" border="0" alt="SourceForge.net Logo"
-    /></a>
-
+      <!--#include file="nav.html"-->
       </td>
       <td width="80%" valign="top">
       <!-- content -->
 
 <div align="center">
 <p>&nbsp;</p>
-<h1><font class="first">T</font>he
-    <font class="first">A</font>rchive of
-    <font class="first">F</font>ormal
-    <font class="first">P</font>roofs</h1>
+
+<!-- begin entry data: -->
+<h1><!-- Title: -->???</h1>
 <p>&nbsp;</p>
 
-<table width="80%" class="entries">
+<table width="80%" class="data">
   <tbody>
-    <tr><td>
-The Archive of Formal Proofs is a collection of proof libraries, examples,
-and larger scientifc developments, mechanically checked in the theorem prover
-<a href="http://isabelle.in.tum.de/">Isabelle</a>. It is organized in the way 
-of a scientific journal. Submissions are refereed.</td></tr>
+    <tr><td class="datahead" width="20%">Title:</td>
+    <td class="data" width="80%">
+<!-- Title: -->???
+    </td></tr>
+		
+    <tr><td class="datahead">Author:</td>
+<td class="data">
+<!-- Author: --><a
+href="???">???</a>
+</td></tr>		
+    
+	<tr><td class="datahead">Submisison date:</td>
+	
+<td class="data"><!-- Submission date: -->????-??-??</td></tr>
+
+	<tr><td class="datahead" valign="top">Abstract:</td>
+  <td class="abstract"> 
+<!-- Abstract: -->	
+???
+
+   </td></tr>
 </tbody>
 </table>
 
 <p>&nbsp;</p>
 
-<table width="80%" class="entries">
+<!-- entry directory name: -->
+<!--#set var="name" value="???" -->
+
+<!--#set var="doc" value="../browser_info/current/HOL/${name}/document.pdf" -->
+<!--#set var="browse" value="../browser_info/current/HOL/${name}/index.html" -->
+<!--#set var="tar" value="../release/afp-${name}-current.tar.gz" -->
+
+<table class="links">
   <tbody>
     <tr>
-      <td class="head">2004</td>
-    </tr>
-    
-<!-- entry begin --
-<tr><td class="entry">
-??? 2004-MM-DD:&nbsp;&nbsp;
-<a href="entries/???.html">???</a>
-<br>Author:&nbsp;&nbsp;
-<a href="???">???</a>
-</td></tr>
--- entry end -->
-
-<!-- entry begin -->
-<tr><td class="entry">
-2004-02-25:&nbsp;&nbsp;
-<a href="entries/Example-Submission.html">Example Submission</a>
-<br>Author:&nbsp;&nbsp;
-<a href="http://www.cse.unsw.edu.au/~kleing/">GerwinKlein</a>
-</td></tr>    
-<!-- entry end -->
-
+  <td class="links">
+	<a href="<!--#echo var="doc" -->">Proof document</a>
+  </td>
+	<!-- link to README.hmtl if no document exists -->	
+	</tr>
+    <tr>
+  <td class="links">
+	<a href="<!--#echo var="browse" -->">Browse theories</a>
+	</td></tr>
+    <tr>
+  <td class="links"> 
+	<a href="<!--#echo var="tar" -->">Download this entry</a>
+	</td>
+  </tr>
+    <tr><td class="links">Older releases:	None</td></tr>
   </tbody>
 </table>
+<!-- entry data end -->
 
 </td> </tr> </table>
-</body>
+<div align="right" class="date">$Date: 2004-02-27 01:26:46 $, $Revision: 1.1 
+$</div></body>
 </html>
web/about.html to web/about.shtml
--- a/web/about.html
+++ b/web/about.shtml
@@ -13,31 +13,8 @@
   <tbody>
     <tr>
       <td width="20%" align="center" valign="top">
-      <!-- navigation -->
-
-	  <p> </p>
-
-	  <a href="http://isabelle.in.tum.de"><img src="images/isabelle.png"
-width="100" height="86" border=0></a>
-	  <p> </p>
-	  <p> </p>
-
-	  <table class="nav">
-      <tr><td class="nav" width="100%"><a href="index.html">Home</a> </td></tr>
-      <tr><td class="nav"><a href="about.html">About</a> </td></tr>
-      <tr><td class="nav"><a href="submitting.html">Submission Guidelines</a>
-</td></tr>      <tr><td class="nav"><a href="search.html">Search</a> </td></tr>
-      <tr><td class="nav"><a href="download.html">Download</a> </td></tr>
-      </table>
-
-	  <p> </p>
-	  <p> </p>
-	<a
-    href="http://sourceforge.net"><img
-    src="http://sourceforge.net/sflogo.php?group_id=101909&amp;type=1"
-    width="88" height="31" border="0" alt="SourceForge.net Logo"
-    /></a>
-
+  <!-- navigation -->
+  <!--#include file="nav.html"-->
       </td>
       <td width="80%" valign="top">
       <!-- content -->
@@ -58,7 +35,7 @@
 <p>The Archive of Formal Proofs is a collection of proof libraries, examples,
 and larger scientific developments, mechanically checked in the theorem prover
 <a href="http://isabelle.in.tum.de/">Isabelle</a>. It is organized in the way
-of a scientific journal. <a href="submitting.html">Submissions</a> are
+of a scientific journal. <a href="submitting.shtml">Submissions</a> are
 refereed.</p>
 
 <p>The archive is hosted by <a href="http://sourceforge.net">sourceforge</a> to
@@ -69,10 +46,10 @@
 <h2>Editors</h2>
 <p><a name="editors">The editors of the archive are</a></p>
 <ul>
+<li><a href="http://www.cse.unsw.edu.au/~kleing/">Dr. Gerwin Klein</a>,
+    <a href="http://www.nicta.com.au">National ICT Australia</a></li>
 <li><a href="http://www4.in.tum.de/~nipkow/">Prof. Tobias Nipkow</a>,
     <a href="http://www.tum.de/">Technische Universität München</a></li>
-<li><a href="http://www.cse.unsw.edu.au/~kleing/">Dr. Gerwin Klein</a>,
-    <a href="http://www.nicta.com.au">National ICT Australia</a></li>
 <li><a href="http://www.cl.cam.ac.uk/users/lcp/">Prof. Larry Paulson</a>,
     <a href="http://www.cam.ac.uk/">University of Cambridge</a></li>
 </ul>
web/submitting.html to admin/regression
--- a/web/submitting.html
+++ b/admin/regression
@@ -1,97 +1,182 @@
-<!DOCTYPE public "-//w3c//dtd html 4.01 transitional//en"
-		"http://www.w3.org/TR/html4/loose.dtd">
-<html>
-<head>
-  <title>The Archive of Formal Proofs</title>
-  <link rel="stylesheet" type="text/css" href="front.css">
-  <meta http-equiv="Content-Type" content="text/html; charset=iso-8859-1">
-  <meta name="GENERATOR" content="Quanta Plus">
-</head>
-<body>
+#!/usr/bin/env bash
+#
+# $Id: regression,v 1.1.2.15 2004-03-29 07:18:56 lsf37 Exp $
+# Author: Gerwin Klein, NICTA
+# License: GPL (GNU GENERAL PUBLIC LICENSE)
+#
+# Automated regression test to be run from cron.
+# Sends email to maintainers if test fails.
+#
+# Relies on beind run in the isatest environment.
+# 
 
-<table width="100%">
-  <tbody>
-    <tr>
-      <td width="20%" align="center" valign="top">
-      <!-- navigation -->
+. ~/.bashrc
 
-	  <p> </p>
+## settings
 
-	  <a href="http://isabelle.in.tum.de"><img src="images/isabelle.png"
-width="100" height="86" border=0></a>
-	  <p> </p>
-	  <p> </p>
+ISABELLE_RELEASES=/usr/proj/isabelle
+ISABELLE_DEVEL=~/isadist/Isabelle
+WORKING_COPY=~/afp
+DATE=$(date "+%Y-%m-%d")
 
-	  <table class="nav">
-      <tr><td class="nav" width="100%"><a href="index.html">Home</a> </td></tr>
-      <tr><td class="nav"><a href="about.html">About</a> </td></tr>
-      <tr><td class="nav"><a href="submitting.html">Submission Guidelines</a>
-</td></tr>      <tr><td class="nav"><a href="search.html">Search</a> </td></tr>
-      <tr><td class="nav"><a href="download.html">Download</a> </td></tr>
-      </table>
+LOG=~/afp-log/afp-test
+MASTERLOG=~/afp-log/afp-test.log
+REPORT=~/afp-log/report
 
-	  <p> </p>
-	  <p> </p>
-	<a
-    href="http://sourceforge.net"><img
-    src="http://sourceforge.net/sflogo.php?group_id=101909&amp;type=1"
-    width="88" height="31" border="0" alt="SourceForge.net Logo"
-    /></a>
+SHORT=sun-poly
+SETTINGS=~/settings/$SHORT
 
-      </td>
-      <td width="80%" valign="top">
-      <!-- content -->
+TMP=/tmp/regression.mail.tmp
+while [ -e $TMP ]; do TMP=$TMP.x; done
 
-<div align="center">
-<p> </p>
-<h1><font class="first">S</font>ubmission
-    <font class="first">G</font>uidelines</h1>
-<p> </p>
+#
+PRG="$(basename "$0")"
 
-<table width="80%" class="descr">
-  <tbody>
-    <tr><td>
-    <p>Please send your submissions by email to
-    <tt>&lt;afp-submit at in.tum.de&gt;</tt>.</p>
+## functions
 
-    <p>The submission should contain</p>
-    <ul>
-    <li>Title, authors and abstract in plain text.</li>
-    <li>A name. It will become the directory name of the archive
-    entry.</li>
-    <li>Name/contact of the maintainer of the entry (usually the author).</li>
-    <li>URL or email address of authors to display on the web page.</li>
-    <li>A tar file with the theory files, IsaMakefile, ROOT.ML and README or
-        document directory. The theories should work with the current
-        release of <a href="http://isabelle.in.tum.de/">Isabelle</a>.
-    <li>A notice that you license your submission under LGPL if accepted.</li>
-    </ul>
+function usage()
+{
+  echo
+  echo "Usage: $PRG [-|release_tag]"
+  echo
+  echo "  Runs testall from cron and logs output"
+  echo 
+  exit 1
+}
 
-    <p>There is a <a href="submit-template">submission template</a>
-    available and an
-     <a href="entries/Example-Submission.html">example submission</a>
-    that contains further information.</p>
+function fail()
+{
+  echo "$1" >&2
+  exit 2
+}
 
-    <p>It is possible and encouraged to build on other archive entries
-       in your submission</p>
+## 
 
-    <p>Your submission will be refereed and you will receive notification
-    as soon as possible. If accepted, you must agree to maintain your
-    archive entry or nominate someone else to maintain it. The Isabelle
-    development team will assist with maintenance, but it does not have the
-    resources to fully maintain the complete archive.</p>
+[ "$#" != "1" -o "$1" = "-?" ] && usage
 
-    <p>If you have questions regarding your submission please contact the <a
-       href="about.html#editors">editors</a>.
-      If you need help with Isabelle, please use the
-<a href="mailto:isabelle-users@cl.cam.ac.uk">isabelle-users@cl.cam.ac.uk</a>
-      mailing list. It is always a good idea to <a
-      href="mailto:lcp@cl.cam.ac.uk">subscribe</a>.</p>
-</td></tr>
+if [ "$1" == "-" ]; then
+  TAG="-A"
+  AFP_VER="development"
+  WORKING_COPY=$WORKING_COPY/devel
+  ISATOOL=$ISABELLE_DEVEL/bin/isatool
+    
+  ERRORDIR=$HOME/var
+  ERRORLOG=$ERRORDIR/error.log
+  RUNNING=$HOME/var/running
+  shopt -s nullglob
+  if [ -n "$(ls $RUNNING)" -o -e $ERRORLOG ]; then
+    echo "`date`: Skipped test. Isabelle devel version broken." >> $MASTERLOG
+    exit 1
+  fi
+  cat $SETTINGS >> $ISABELLE_DEVEL/etc/settings
+  ML_IDENTIFIER=`$ISATOOL getenv -b ML_IDENTIFIER` || fail "could not identify ML system"
+  export ISABELLE_IMAGE_PATH="$HOME/isabelle-$SHORT/heaps/$ML_IDENTIFIER/"
+  LOG=$LOG-devel-$DATE.log
+  SNAPSHOT=1;
+  REPORT=$REPORT-devel
+else
+  TAG="-r $1"
+  AFP_VER="release ($1)"
+  WORKING_COPY=$WORKING_COPY/release
+  ISATOOL=$ISABELLE_RELEASES/$1/bin/isatool
+  LOG=$LOG-$1-$DATE.log
+  REPORT=$REPORT-$1
+fi
 
-</tbody>
-</table>
+. $WORKING_COPY/admin/main-config || fail "could not read main-config."
+MAIL=$WORKING_COPY/admin/mail-attach
 
-</td> </tr> </table>
-</body>
-</html>
+echo "Start test at `date`" > $LOG
+echo >> $LOG
+echo "begin cvs update" >> $LOG
+
+# cvs update to newest version of archive 
+cd $WORKING_COPY || fail "could not cd to $WORKING_COPY"
+cvs -q up -P -d $TAG >> $LOG 2>&1 || fail "could not CVS update."
+
+echo "end cvs update" >> $LOG
+echo >> $LOG
+
+# run test
+nice $WORKING_COPY/admin/testall -t $ISATOOL -c >> $LOG 2>&1
+FAILURE=$?
+
+ELAPSED=$("$HOME/bin/showtime" "$SECONDS")
+
+echo >> $LOG
+echo "End test on `date`, elapsed time: $ELAPSED" >> $LOG
+
+# generate report
+DIFF=`$WORKING_COPY/admin/report.pl $LOG $REPORT`
+
+# send mail on status changes
+if [ -n "$DIFF" ]; then
+  cat > $TMP <<EOF
+The status of the following AFP entries changed:
+$DIFF
+
+Tested version: $AFP_VER
+Test ended on: $HOSTNAME, `date`.
+
+Have a nice day,
+  isatest
+
+EOF
+  for R in $MAIN_NOTIFY; do
+    $MAIL 'status changed (AFP)' "$R" $TMP $REPORT $LOG
+  done  
+  # do not send duplicate mail
+  MAIN_NOTIFY=""
+fi
+
+# send email to maintainer if there was a problem
+if [ "$FAILURE" != "0" ]; then
+  FAIL=`tail -4 $LOG | head -1`
+  echo "`date`, $AFP_VER: test failed on [$FAIL]. Elapsed time: $ELAPSED" >> $MASTERLOG
+  for E in $FAIL; do
+    (
+      . $WORKING_COPY/thys/$E/config || fail "error reading config for $E"
+      if [ "$FREQUENT" == "yes" ]; then
+        cat > $TMP <<EOF
+Session [$E] in the automated afp test failed. 
+Tested version: $AFP_VER
+Test ended on: $HOSTNAME, `date`.
+
+To reproduce the error, check out the $AFP_VER version of the
+archive from sourceforge and run "isatool make" on your session.
+
+This is an automatically generated email. To switch off these 
+notifications, edit thys/$E/config and cvs commit the changes.
+
+Have a nice day,
+  isatest
+
+EOF
+        for R in $NOTIFY $MAIN_NOTIFY; do
+          $MAIL 'test failed (Archive of Formal Proofs)' "$R" $TMP $LOG
+        done
+      fi
+    )
+  done
+else
+  echo "`date`, $AFP_VER: All tests successful. Elapsed time: $ELAPSED" >> $MASTERLOG
+fi
+
+# clean up tmp
+rm -f $TMP
+
+# make devel snapshot
+if [ "$SNAPSHOT" == "1" ]; then
+    EXPORT=afp-devel
+    STATUS=entry-status.txt
+    WEB=~/html-data/afp
+    cp $REPORT $WEB/$STATUS
+    cvs -Q export -D now -d $EXPORT thys
+    cp $REPORT $EXPORT/$STATUS
+    echo >> $EXPORT/$STATUS
+    echo `date` >> $EXPORT/$STATUS
+    tar cf $EXPORT.tar $EXPORT
+    gzip --best -f $EXPORT.tar
+    mv $EXPORT.tar.gz $WEB
+    rm -rf $EXPORT
+fi
1 2 3 > >> (Page 1 of 3)