[isabelle-dev] How to activate/de-activate unifier-trace from ML-level
makarius at sketis.net
Tue Feb 10 18:30:32 CET 2015
On Tue, 4 Nov 2014, Makarius wrote:
> Strange hacks that work around the absence of proper options encumber
> the introduction of them eventually. It is the usual bootstrap problem
> for reforms.
> I actually did start some work in the vicinity of resolve_tac with
> proper context recently, but it will require more time to revisit really
> ancient parts of the system, not to say ancient habits.
Here is an update on this pending thread: current Isabelle/50b60f501b05 is
the main move to proper context for resolve_tac etc. After endless years
of preparation to "localize" the majority of Isabelle tools, it turned out
a releatively small change.
What remains are slightly odd entry points without context:
resolve0_tac/rtac, eresolve_tac/etac, dresolve_tac/dtac. We could
probably remove them altogether, but there are a lot of remaining uses in
the new datatype implementation, which I don't want to change myself.
More information about the isabelle-dev