On Mon, 15 Jul 2013, Dmitriy Traytel wrote:
"Code generator: dropping subsumed code equation" by Auto Quickcheck
I guess it would be the task the tools to omit such outbursts and not
globally on the IDE side?
In principle Context_Position.is_visible should control that, and the
tools should observe it accordingly. I will take a few more rounds of
looking at the current collection of tools we have right now; solve_direct
should be also able to contain itself, without too much spamming.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
