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 applications.
How to write a tactic resolve_with_tracing: thm list -> int -> tactic that behaves like resolve_tac, but outputs unification trace? Best, Peter p.s. Not sure whether this belongs to user or devel, but the reason for my message is http://sourceforge.net/p/afp/code/ci/7189f7ffd73e17c2395eb552c89004f5b8e0453e/ which seems to be related to tty-mode elimination that is currently going on in dev-version. _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
