[isabelle] Finding theorems via intro
when using Isabelle's feature to search for theorems I frequently use
the "intro" command instead of a pattern to find the appropriate
introduction rule for inductively defined sets. Actually, I would like
to get the names of the introduction rules that match, i.e. those names
that I explicitly gave these rules in the inductive declaration.
However, the search result does not contain these names, but
....intros(23): ..., ....intros(34): ..., etc., which is not what I
wanted in the first place because the rules' positions in the inductive
definition are not stable when I add/delete/move some rules.
Is there some switch in Isabelle 2008 to make Isabelle display the
rules' names that are given explicitly in the inductive definition?
As a concrete example, take
lemma "(a, a) : r^*"
Doing a search for "intro" theorems, this gives (among many others)
Transitive_Closure.rtrancl.intros(1): (?a, ?a) : r^*
However, I would like to get:
Transitive_Closure.rtrancl.rtrancl_refl: (?a, ?a) : r^*
This archive was generated by a fusion of
Pipermail (Mailman edition) and