[isabelle-dev] Abbreviations and find_theorems

[Christian Sternagel]

Hi Florian,

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.

cheers

chris

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.
>
> Cheers,
> 	Florian
>
>
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>