[isabelle-dev] NEWS: 'interpret' vs. literal facts and locale performance

[Makarius]

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 interpretation are always lazy, unless there
are attributes attached to them (this requires to update the context on
the spot, e.g. a [simp] declaration).

Global facts within the theory will always be forced in the final
consolidation of (forked) proofs that have been recorded. In particular,
 a session image will have all facts stored in evaluated form.

Local facts stemming from hypothetical interpretations (e.g. 'interpret'
within a proof, probably also 'sublocale') are only forced when they get
used. When the local context closes, there is no permanent result.

This explains, why I did not add anything to the NEWS concerning lazy
facts -- these details should not relevant to users, everything should
work as before.


	Makarius