[isabelle] Application order of (safe) introduction rules



Hi all,

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 the list.
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 by accident?
How is the behavior with (auto intro: test), which lemma is tried first?


Best,
 Peter






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