[isabelle-dev] »Find theorems«-Panel

[Makarius]

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 ...


 	Makarius