# [isabelle] intro and types

Hi there!

`I am currently reading through some Isabelle/HOL formalizations that
``I've been doing over the last few years. Doing that, I discovered the
``following: It is sometimes convenient to have specialized rules for more
``specific types. For example I use
`
lemma subsetI2: assumes "!!x y. (x,y) : S ==> (x,y) : T" shows "S <= T"

`rather often at the beginning of some proof (usually about binary
``relations). That is, a corresponding proof starts as follows:
`
proof (rule subsetI2)
What I would like to have instead is
proof

`Now, declaring subsetI2 as 'intro' doesn't help. Still, the more general
``rule subsetI is used. So my question is, how do I specify, when several
``rules would be applicable, which one is used by the 'rule' method? The
``same problem arises, when there are several introduction rules for some
``constant. As far as I figured out, as long as the types are at the same
``level (in contrast to the above subsetI2, where the original rule can be
``applied on 'a set, but subsetI2 can only be applied on ('a * 'a)set),
``the order in which rules are declared as 'intro' does matter. Is that
``correct or was it just a coincidence in my case?
`
best regards
chris

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