Re: [isabelle] Application order of (safe) introduction rules
On Thu, 9 Jun 2011, Lawrence Paulson wrote:
It has been a very long time since I worked on this, but I believe that
indeed the order is taken under strict account. Back in the days of ML,
blah_cs addSIs [lemma1]
was guaranteed to give priority to lemma1 over the other theorems in
blah_cs. The code that keeps track of the order in which theorems are
delivered is still there.
Concerning the old-style addXX declarations there is a subtle point here,
that I've only realized rather late in 1998/99 when introducing the
When you write in Isar
(fast intro: thm1 thm2)
the order of declarations is from left to right, so the later one takes
precedence: thm2 before thm1.
When you write in ML
fast_tac (cs addSIs [thm1, thm2])
the declaration order is inside out (using fold_rev internally), so you
get thm1 before thm2.
This provided some potential for actual confusion 10 years ago, but now
the old addXX declarations are so rare in practice that it is much less
This archive was generated by a fusion of
Pipermail (Mailman edition) and