[isabelle-dev] How to activate/de-activate unifier-trace from ML-level

[Dmitriy Traytel]

Hi Makarius,

On 10.02.2015 18:30, Makarius wrote:
> 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.

indeed approximately 2/3 of all usages of rtac in the Isabelle 
distribution + AFP are in our BNF tactics (roughly 2000 occurrences).

Adding a context to each of them would make the tactics even harder to 
read/maintain compared to their current state. The only decent way of 
adding the context everywhere would be via some combinators à la

THEN'': (ctxt -> int -> tactic) * (ctxt -> int -> tactic) -> ctxt -> int 
-> tactic

assuming that rtac has type "thm -> ctxt -> int -> tactic"

or reuse the polymorphism of THEN'  and work with an uncurried version 
of rtac: thm -> (ctxt, int) -> tactic (and other tactics). Needless to 
say that I could do this only locally in the BNF package, but maybe this 
is a general question of how tactics should look like.

Dmitriy