[isabelle-dev] »Find theorems«-Panel
makarius at sketis.net
Tue Sep 24 22:24:24 CEST 2013
On Thu, 5 Sep 2013, Florian Haftmann wrote:
> At some stage I would expect some »click and copy to theory buffer«
> functionality, e. g.
> thm foo
> from foo have "<prop>" .
I would say that is another instance of "structured editing". Output
should provide systematic markup about the "Isabelle sublanguage" that is
being used, e.g. "fact expression". Copy-pasting that should do the right
thing, depending on the syntactic context of the target.
This is for *some* future release ...
More information about the isabelle-dev