[isabelle-dev] Abbreviations and find_theorems

[Gerwin Klein]

I agree that it would be nice to support that, esp since find_theorems is supposed to help beginners find things.

Applying underscores will have unwanted side effects for other terms, esp constants, though, so one would have to be careful to apply this to abbreviations only. AFAIR this is the reason nobody has done it yet.

Cheers,
Gerwin


> On 16.11.2014, at 04:04, Christian Sternagel <c.sternagel at gmail.com> wrote:
>
> 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
>>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.