[isabelle-dev] Abbreviations and find_theorems

[Florian Haftmann]

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

As it is »by now«, search patterns in find_theorems are not matched
modulo eta-conversion.

I see two technical solutions to resolve this:
a) Make the underlying pattern match implementation work modulo
eta-conversion.
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.

Cheers,
	Florian

-- 

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20141204/9ed5896f/attachment.asc>