[isabelle] Disabling the record simprocs
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
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
This archive was generated by a fusion of
Pipermail (Mailman edition) and