On Fri, 19 Jul 2013, Tobias Nipkow wrote:
I have generalized the concept to allow changing the visibility of a
global theory context as well. This is observed by unify.ML, as a
guard to its many tracing options, find_theorems.ML then copies the
Proof.context visibility over to a copy of the background theory of the
goal state, so 'solve_direct' no longer produces spam from this source,
see Isabelle/d68fd63bf082.
Does that mean that one could add an attribute unify_trace now?
These have been there since 2007:
changeset: 24178:4ff1dc2aa18d
user: wenzelm
date: Tue Aug 07 20:19:55 2007 +0200
files: src/HOL/Bali/Basis.thy src/HOL/IMPP/Natural.thy
src/HOL/Induct/Com.thy src/HOL/MicroJava/J/JTypeSafe.thy
src/Pure/Isar/attrib.ML src/Pure/unify.ML
src/Sequents/LK/Hard_Quantifiers.thy src/Sequents/ROOT.ML
src/Sequents/Sequents.thy
description:
turned Unify flags into configuration options (global only);
The "global only" aspect is a source of confusion and potential problems,
but it cannot be changed: unification is routinely applied without a
proper context, e.g. in "RS".
What I have done in 51dfdcd88e84 is to make
Context_Position.is_visible_global a guard for *any* output of the
unify.ML module -- it is quite complex in its chatty manner, and that way
we know that it cannot produce outbursts that bomb the prover front-end
for tools that can afford to change the global theory to disable context
visibility.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
