[isabelle-dev] Abbreviations and find_theorems

Timothy Bourke tim at tbrk.org
Wed Nov 26 21:16:47 CET 2014


* Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> [2014-11-26 19:40 +0100]:
> @Timothy: in the progress of investigating I stumbled over your
> changeset (c61fe520602b, actually brought in by Gerwin) and dismantled
> it.  Do you remember what it had been intended for resp. by which
> criterion we can decide whether the dismantling is really admissible?
> Before going ahead and pushing something, I would like to resolve this
> question.

I'm afraid that I cannot recall anything about this changeset. Sorry!

As far as I'm concerned, you may proceed as best you see fit.

Tim.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 473 bytes
Desc: Digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141126/1bd27147/attachment.sig>


More information about the isabelle-dev mailing list