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
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
