*To*: miramirkhani at ce.sharif.edu*Subject*: Re: [isabelle] finding a rule*From*: Brian Huffman <brianh at cs.pdx.edu>*Date*: Tue, 20 Apr 2010 06:49:28 -0700*Cc*: cl-isabelle-users at lists.cam.ac.uk*In-reply-to*: <1217.213.233.170.191.1271745739.squirrel@ce.sharif.edu>*References*: <1217.213.233.170.191.1271745739.squirrel@ce.sharif.edu>*Sender*: huffman.brian.c at gmail.com

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

**References**:**[isabelle] finding a rule***From:*miramirkhani

- Previous by Date: [isabelle] Automatheo 2010 at FLoC: Final Call for Papers, Talks, and System Demonstrations
- Next by Date: Re: [isabelle] Questions about . method
- Previous by Thread: Re: [isabelle] finding a rule
- Next by Thread: [isabelle] Automatheo 2010 at FLoC: Final Call for Papers, Talks, and System Demonstrations
- Cl-isabelle-users April 2010 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list