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_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
