On Wed, 31 Jul 2013, Makarius wrote:
* Type theory is now immutable, without any special treatment of
drafts or linear updates (which could lead to "stale theory" errors in
the past). Discontinued obsolete operations like Theory.copy,
Theory.checkpoint, and the auxiliary type theory_ref. Minor
INCOMPATIBILITY.
Here are some further explanations on this:
Tools may now update a theory value locally in arbitrary ways, i.e. to
explore certain situations that are given up later on (e.g. to see if a
type may be declared without producing an error).
What does *not* work is to update the background theory of some proof
context, and then continue deriving results from it. There is no "export"
from such adhoc theory extensions, so the result would live in the
extended theory and cannot be transferred back. This also explains why
theory and Proof.context are different things, and why a background theory
is not a proper context. (Interestingly, Coq has only one context, and
tools occasionally extend that globally during proof construction, leading
to great confusion and bad performance.)
This fine point about theory update is also relevant to
Context_Position.set_visible_global: solve_direct can afford changing the
theory locally to silence certain internal operations, since it merely
retrieves existing results without deriving results. General proof tools
(e.g. tactics) cannot do that since the final result needs to be from the
original theory.
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
