[isabelle] Application order of (safe) introduction rules
I have a list of lemmas:
lemmas test = l1 l2 ... ln
some of the lemmas are specializations of the other lemmas, i.e. l2 =
l1[where f=id, simplified], such that
l1 matches everywhere where l2 matches, but, of course, I want to use l2
where ever possible.
now I do:
apply (auto intro!: test)
the result of the proof seems to depend on the order of the lemmas in
To me, it seems that intro! applies the *last* matching lemma from test.
Is this the documented (reliable on) behavior, or is this behavior just
How is the behavior with (auto intro: test), which lemma is tried first?
This archive was generated by a fusion of
Pipermail (Mailman edition) and