Following a recent hint (cited at the bottom below) I tried to inspect
(in Isabelle2014), which rewrite rules are used by "auto" for proving
lemma "(∃x. ∀y. P x y) ⟶ (∀y. ∃x. P x y)"
using [[simp_trace_new mode=full]]
using [[simp_break "_ ⟶ _"]]
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,
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and