[isabelle] simp_trace_new



Following a recent hint (cited at the bottom below) I tried to inspect (in Isabelle2014), which rewrite rules are used by "auto" for proving this lemma:

lemma "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
using [[simp_trace_new mode=full]]
using [[simp_break "_ ⟶ _"]]
by auto

With focus on "auto" <Output> indeed shows

lemma (∃x. ∀y. ?P x y) ⟶ (∀y. ∃x. ?P x y)
See <simplifier trace>

but klicking "<simplifier trace>" opens two empty windows.

Now I don't know whether
* "auto" doesn't need the simplifier in the above proof
* there is something I am doing wrong
* the hint below does not yet apply to Isabelle2014.

Thanks a lot in advance,
Walther


PS: "isar-ref" explains "simp_trace_new" and "simp_break", but my questions above remain; in "jedit" I found no match.


On 14-11-28 03:25 PM, Tobias Nipkow wrote:
:
:
How to find out? Put "using [[simp_trace_new mode=full]]" in front of your simp/auto command.

Tobias






This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.