aboutsummaryrefslogtreecommitdiff
path: root/html
diff options
context:
space:
mode:
authorDavid Aspinall2002-05-03 13:34:55 +0000
committerDavid Aspinall2002-05-03 13:34:55 +0000
commitf33b1cb972d0d19708fc30f11d9722f353b7faa4 (patch)
treea1b557093fb285afcb6ef885d886266727934d72 /html
parente305fa187464fa1a8e3f90b6625339c13a625dd1 (diff)
New files.
Diffstat (limited to 'html')
-rw-r--r--html/eproofe5
-rw-r--r--html/eproofe.php30
2 files changed, 35 insertions, 0 deletions
diff --git a/html/eproofe b/html/eproofe
new file mode 100644
index 00000000..2df23c96
--- /dev/null
+++ b/html/eproofe
@@ -0,0 +1,5 @@
+<?php include('eeproof.php'); ?>
+<?php
+ /* This file needs some extra characters in it for apache to work its magic.
+ Things work fine as link to index.html, but it's tricky to include links
+ in cvs. */ ?>
diff --git a/html/eproofe.php b/html/eproofe.php
new file mode 100644
index 00000000..e965a78a
--- /dev/null
+++ b/html/eproofe.php
@@ -0,0 +1,30 @@
+<?php
+ require('functions.php3');
+ small_header("Engineering Electronic Proof");
+ ?>
+
+<p>
+Proof General, and particularly, the <a href="kit">Proof General
+Kit</a> is proposed as a vehicle for research into <i>engineering
+electronic proof<i>. We want to investigate the
+maintenance, combination, and reuse of formal proof developments.
+</p>
+
+<h3>Planning</h3>
+<p>
+This project has not yet been started, and there are no public
+documents available yet.
+</p>
+<p>
+Some hints of our plans appear in the papers describing
+the <a href="kit">Proof General Kit</a>.
+</p>
+
+<p>
+Any <a href="mailto:da@dcs.ed.ac.uk">comments</a> are welcomed.
+</p>
+
+<?php
+ click_to_go_back();
+ footer();
+?>