From b37bf74fc2d6309a5ae3dc6b55e8488409976775 Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Tue, 29 Feb 2000 06:19:39 +0000
Subject: New projects directory.

---
 html/projects/isapbp.html | 25 +++++++++++++++++++++++++
 1 file changed, 25 insertions(+)
 create mode 100644 html/projects/isapbp.html

(limited to 'html/projects/isapbp.html')

diff --git a/html/projects/isapbp.html b/html/projects/isapbp.html
new file mode 100644
index 00000000..c08ea85e
--- /dev/null
+++ b/html/projects/isapbp.html
@@ -0,0 +1,25 @@
+<h2>Proof-by-pointing support for Isabelle</h2>
+<p>
+Isabelle has a sophisticated concrete syntax mechanism which makes it
+difficult to add annotations to connect the displayed output back to
+the internal abstract syntax.  This issue needs to be solved to
+support proof-by-pointing (and other features) in Isabelle.
+A 
+<a href="http://www.informatik.uni-bremen.de/~bu/isa_contrib/isabelle.html">
+patch by Burkhart Wolff</a> 
+providing term structure annotations for a previous release of
+Isabelle may be useful here.  To implement proof-by-pointing itself,
+tactics using the gesture information must be written.
+</p>
+<p>
+<b>Skills:</b>
+ Some understanding of Isabelle implementation, 
+ co-operation with the Isabelle developers to get
+ Isabelle modifications incorporated.
+ Skill in writing Isabelle tactics.
+ Minimal Emacs Lisp knowledge.
+</p><p>
+<b>Proposer:</b>
+<a href="http://zermelo.dcs.ed.ac.uk/~da">David Aspinall</a>.
+</p>
+
-- 
cgit v1.2.3