# Re: [isabelle] simp_trace_new

```Hi David,

thanks a lot for your reply to my questions in isabelle-users@ ...
```
```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
* "simp_trace_new mode=full" does not yet apply to Isabelle2014.
```
```If the simplifier trace doesn't help you, you might want to look
at Daniel Matichuk's "apply_trace" command, which I have described
at:
http://stackoverflow.com/a/26827242/570879
```
```... this looks great ...

```
```(* attempt 5 to watch *)
lemma "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
apply_trace auto
done
(*used theorems:
allE: ∀x. ?P x ⟹ (?P ?x ⟹ ?R) ⟹ ?R
allI: (⋀x. ?P x) ⟹ ∀x. ?P x
ccontr: (¬ ?P ⟹ False) ⟹ ?P
exE: ∃x. ?P x ⟹ (⋀x. ?P x ⟹ ?Q) ⟹ ?Q
exI: ?P ?x ⟹ ∃x. ?P x
impI: (?P ⟹ ?Q) ⟹ ?P ⟶ ?Q
swap: ¬ ?P ⟹ (¬ ?R ⟹ ?P) ⟹ ?R *)
```
```
```
... and seems to give a negative answer to our ultimate question: Can we have a "naive mathematician's approach" to simple quantifier reasoning in Isabelle without delving down to the meta-logic?
```
Walther

```

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