On 25/02/18 13:32, Makarius wrote:
> various performance improvements of the locale infrastructure leading up
> to that changeset (e.g. performance tuning for instantiate_free
> operations and lazy entries in the facts environment).
Some more notes on this.
Facts emerging from locale
*** Isar ***
* Command 'interpret' no longer exposes resulting theorems as literal
facts, notably for the \prop\ notation or the "fact" proof
method. This
improves modularity of proofs and scalability of locale interpretation.
Rare INCOMPATIBILITY, need to refer to explicitly named facts instead
