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

Peter Lammich lammich at in.tum.de
Mon Nov 3 09:40:21 CET 2014

Hi List,

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 mailing list