Email Gateway (Aug 19 2022 at 08:01): Email Gateway (Aug 19 2022 at 08:01):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
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
“[1]Adding rewrite rule "??.unknown":”
For a concrete case I just had, there were multiple
[1]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
Email Gateway (Aug 19 2022 at 08:02):From: Tobias Nipkow <nipkow@in.tum.de>
This has nothing to do with jedit. Simplification is an interative process that
may traverse the proof state multiple times. Hence the same premise may be
inserted into the context multiple times, and each time you are notified. We
apologize for any inconvenience this may cause.
Tobias
Email Gateway (Aug 19 2022 at 08:02):From: "Yannick Duchêne (Hibou57 )" <yannick_duchene@yahoo.fr>
Hi Tobias,
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
complaining.
Last updated: Nov 21 2024 at 12:39 UTC