* 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. _______________________________________________ Isabelle-dev mailing list Isabelle-dev@mailbroy.informatik.tu-muenchen.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
