New projects directory.

1 files changed, 25 insertions, 0 deletions

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>
+