Re: [isabelle] finding a rule

On Mon, Apr 19, 2010 at 11:42 PM,  <miramirkhani at> wrote:
> Dear all,
> I'm new to Isabelle and I am about to begin reading some proofs, can any
> one tell me how can I find a specific applied rule by its name?
> ps: ex: apply(possibility), what is possibility?

Given a theorem name, you can display the theorem using Isabelle's
"thm" command. For example,

thm conjI

prints this:

[| ?P; ?Q |] ==> ?P & ?Q

You can type the "thm" command into a theory file and then step over
it (this works either between lemmas or within proofs). Otherwise, if
you don't want to change the file itself, in ProofGeneral you can
press ctrl-c, ctrl-v, and then type a "thm" command into the

Hope this helps,

- Brian

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