[isabelle-dev] Discovering named_theorems
Gerwin.Klein at nicta.com.au
Wed May 11 01:13:47 CEST 2016
> 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
> find dynamic facts as well, but static ones are preferred;
> It is not precisely what you have described, but it is a
> straight-forward continuation of the existing fact retrieval.
> 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.
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.
More information about the isabelle-dev