[isabelle-dev] Abbreviations and find_theorems
florian.haftmann at informatik.tu-muenchen.de
Thu Dec 4 09:36:47 CET 2014
>> The abstraction expansion would basically mean you can’t search for abstractions at all any more. I.e. even something like (%_. _) would be expanded into (_ _). That’s not necessarily catastrophic, but probably counter-intuitive.
>> Has anyone apart from me ever searched for an abstraction that was not an abbreviation? If yes, why?
> Well, there are parts of the system without implicit eta-conversion, and
> some with. I personally would not bother about find patterns working
> modulo eta-conversion implicitly.
Silence has fallen on this thread. Let me put the matter into a more
As it is »by now«, search patterns in find_theorems are not matched
I see two technical solutions to resolve this:
a) Make the underlying pattern match implementation work modulo
b) Expand the search patterns themselves, as proposed above.
Why I have been reluctant to implement a) is that this would complicate
a potentially time-critical code. Hence the more pragmatic solution b).
So, which path is better to follow from now? In case of doubt, we can
choose b) and still later get back to it.
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 181 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev