Re: [isabelle] finding a rule



Either you are using, e.g., 'grep' to search the source files for the name, or better, use the command

  find_theorems name:"possibility"

inside the emacs buffer to search for all theorems/lemmas whose name contains the string "possibility." Note the, e.g., when you have

  apply(rule conjI)

you just search for "conjI" not including "rule ."

cheers

chris

On 04/20/2010 08:42 AM, 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?

Regards

--
Najma









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