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.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
