[isabelle-dev] »Find theorems«-Panel

Makarius 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
> or
> 	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 mailing list