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
