# [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.*