Re: [isabelle] Redundant trace with jEdit
You don't have to apologize. Isabelle as a proof assistant, largely
overweight that kind of issue :-P I just wanted to know, not really
Le Mon, 30 Jul 2012 21:48:58 +0200, Tobias Nipkow
<nipkow at in.tum.de> a écrit:
This has nothing to do with jedit. Simplification is an interative
may traverse the proof state multiple times. Hence the same premise may
inserted into the context multiple times, and each time you are
apologize for any inconvenience this may cause.
Am 30/07/2012 20:02, schrieb Yannick Duchêne (Hibou57):
Hi all the people,
The title mention jEdit, while I'm not sure that's jEdit specific.
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
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
encumbered and less readable.
Is there a known way to filter it out automatically? If possible, I
to have only one trace message for each added rewrite rule. A quick
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