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 ."



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



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