[isabelle] Redundant trace with jEdit
Hi all the people,
The title mention jEdit, while I'm not sure that's jEdit specific. Read:
at least with jEdit.
If ever I create a redundant lemma, Isabelle warns me all the time, even
when I feel it helps readability. But it seems it don't applies the same
to it‑self: whenever I do “using [[simp_trace=true]]” and enable trace in
the output pan, I often get redundant entries starting with
“Adding rewrite rule "??.unknown":”
For a concrete case I just had, there were multiple
Adding rewrite rule "??.unknown":
r x y ≡ True
When repeated multiple times for multiple rewrite rules, this make the
trace encumbered and less readable.
Is there a known way to filter it out automatically? If possible, I would
like to have only one trace message for each added rewrite rule. A quick
search using https://lists.cam.ac.uk/mailman/mmsearch/cl-isabelle-users
returned nothing on that topic.
Have an happy time
“Syntactic sugar causes cancer of the semi-colons.” 
“Structured Programming supports the law of the excluded muddle.” 
: Epigrams on Programming — Alan J. — P. Yale University
This archive was generated by a fusion of
Pipermail (Mailman edition) and