[isabelle] Disabling the record simprocs



Dear list,

For debugging purposes, I'd like to disable the simprocs from the record package. Otherwise, the simplifier trace with [[simp_debug]] is obfuscated by the trace of these simprocs. I tried [[simproc del: "record" record_eq record_upd]], but I only get the error message that none of the simprocs exist. Next, I tried

local_setup {*
  fn ctxt => ctxt delsimprocs [Record.simproc, Record.eq_simproc, Record.upd_simproc]
*}

Then, print_simpset no longer lists these simprocs. Nevertheless, they still show up in the trace. Here's an example:

lemma "foo" using [[simp_debug]] apply(simp)

So, how can I get rid of these simprocs?

By the way, does the new tracing facility for the simplifier provide control over simprocs, too?

Best,
Andreas




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.