[isabelle-dev] NEWS

Sascha Boehme boehmes at in.tum.de
Fri Mar 26 23:48:20 CET 2010

* References 'trace_simp' and 'debug_simp' have been replaced by
configuration options stored in the context. Enabling tracing
(the case of debugging is similar) in proofs works via

  using [[trace_simp=true]]

Tracing is then active for all invocations of the simplifier
in subsequent goal refinement steps.

More information about the isabelle-dev mailing list