[isabelle-dev] Abbreviations and find_theorems

Florian Haftmann florian.haftmann at informatik.tu-muenchen.de
Wed Nov 26 16:12:09 CET 2014

I'm diving into it…


On 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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev


PGP available:

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 181 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20141126/2076cabd/attachment.sig>

More information about the isabelle-dev mailing list