[isabelle-dev] Discovering named_theorems

[Gerwin Klein]

> changeset:   63080:8326aa594273
> tag:         tip
> user:        wenzelm
> date:        Tue May 10 22:25:06 2016 +0200
> files:       src/Pure/Isar/proof_context.ML
> src/Pure/Tools/find_theorems.ML src/Pure/facts.ML
> description:
> find dynamic facts as well, but static ones are preferred;
> tuned;
>
>
> It is not precisely what you have described, but it is a
> straight-forward continuation of the existing fact retrieval.

Nice!


> Note that the "Duplicates" option makes a difference if dynamic facts
> actually show up. The details of these policies are from a different
> continent, and not totally clear to me.

Happy to tweak if it makes sense. What’s there is just what we thought was useful at the time.

Cheers,
Gerwin


________________________________

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.