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,
[| ?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,
This archive was generated by a fusion of
Pipermail (Mailman edition) and