[isabelle-dev] How to activate/de-activate unifier-trace from ML-level
lammich at in.tum.de
Mon Nov 3 09:40:21 CET 2014
I have a tactic that has a debug-mode. In debug-mode,
it shall output unification trace for certain (but not all) rule
How to write a tactic
resolve_with_tracing: thm list -> int -> tactic
that behaves like resolve_tac, but outputs unification trace?
Not sure whether this belongs to user or devel, but the reason
for my message is
which seems to be related to tty-mode elimination that is currently
going on in dev-version.
More information about the isabelle-dev