blob: c08ea85eb2935c7d4bf72e232b6d7145514eec3d (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
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>
|
