[isabelle-dev] Abbreviations and find_theorems

[Florian Haftmann]

I'm diving into it…

	Florian

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:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- 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>