On Wed, 19 Mar 2014, Gerwin Klein wrote:
On 18 Mar 2014, at 10:23 pm, Makarius <makar...@sketis.net> wrote:
Maybe I should try to improve the implicit "rule" method to reveal the rule
that was applied --- via a form of semantic completion. It is a bit more difficult than
the other completions so far, because there is also the lazy enumeration of rules and
rule instantiations involved.
I think beginners would like that, although it does sound like potential
for a fairly deep rabbit hole.
Just for informative purposes it might be not so difficult to turn the
existing Method.rule_trace facility into something that is PIDE compliant
-- also with some filtering of successful rules instead of all candidates.
What is more difficult is to produce text (fact names) that can be
understood by the system again in a robust manner. But I am not quite
up-to-date what the Sledgehammer + Isar output can do already, it might
actually solve that problem.
We have a similar situation with Simplifier trace: the system prints funny
"name hints" (often just "??.unknown"), without clear reference to the
fact name space.
I already know a simple trick to make this into authentic entity
references (with hyperlinks in the output), without requiring proper fact
names (simp rules do not have a name in general.)
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
