[isabelle-dev] Abbreviations and find_theorems
c.sternagel at gmail.com
Sat Nov 15 18:04:04 CET 2014
many month ago I was also surprised, then annoyed, and then I got used
to always adding the "underscore-argument".
I fully agree that users shouldn't have to worry about such technicalities.
On 11/15/2014 05:58 PM, Florian Haftmann wrote:
> Hi all,
> when searching for theorems, abbreviations may behave surprisingly:
> find_theorems "odd _" -- ‹considerable results›
> find_theorems "odd" -- ‹no results›
> I guess this is due to abbreviation expansion which then yields
> find_theorems "λa. odd a" -- ‹no results›
> So, this is formally correct but nevertheless IMHO inconventiently. May
> naive expectation is that when I am searching for a particular
> operations I do not that to think about such technical detail.
> What do others think?
> This refers to 059ba950a657.
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
More information about the isabelle-dev