I'm diving into it…
FlorianOn 21.11.2014 23:56, Makarius wrote: > On Sat, 15 Nov 2014, Gerwin Klein wrote: > >> 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. > > The behaviour of find_theorems in this respect stems from > Pattern.matches_subterm. In 1998 that was introduced for the Simplifier > (6328d427a339), but Stefan Berghofer changed that in his great reform > from 2000 (5b33e732e459). > > So the only use of it is now find_theorems.ML, which means it defines > its intended meaning. You could adapt it accordingly, to find > abstractions in beta-applied form etc. > > If Pattern.matches_subterm changes semantically, the usual way is to > change its name as well. It could also move to find_theorems.ML. > > > Independently of that, current 30b8a5825a9c already moves various > add-ons to pattern.ML and unify.ML to a place where they are outside of > modules that are relevant to the inference kernel. (In the past there > were occasional confusions about what is actually critical code and what > not.) > > > Makarius > > ---------------------------------------------------------------------------- > > http://stop-ttip.org 927,552 people so far > ---------------------------------------------------------------------------- > > _______________________________________________ > isabelle-dev mailing list > isabelle-...@in.tum.de > https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev -- 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
