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