Re: [isabelle] finding a rule



On Mon, Apr 19, 2010 at 11:42 PM,  <miramirkhani at ce.sharif.edu> 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
mini-buffer.

Hope this helps,

- Brian





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