[isabelle] Finding theorems via intro



Hi,

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^*

Andreas





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