From b9caaa8e4b66817dbc66d0e79b567b3285869fea Mon Sep 17 00:00:00 2001
From: David Aspinall
Date: Sat, 7 Feb 2004 19:31:13 +0000
Subject: Deleted file

---
 html/projects/isapbp.html | 25 -------------------------
 1 file changed, 25 deletions(-)
 delete mode 100644 html/projects/isapbp.html

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

diff --git a/html/projects/isapbp.html b/html/projects/isapbp.html
deleted file mode 100644
index c08ea85e..00000000
--- a/html/projects/isapbp.html
+++ /dev/null
@@ -1,25 +0,0 @@
-<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