> 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. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
