diff options
Diffstat (limited to 'html/projects/isapbp.html')
| -rw-r--r-- | html/projects/isapbp.html | 25 |
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> + |