Email Gateway (Aug 18 2022 at 15:08): Email Gateway (Aug 18 2022 at 15:08):From: miramirkhani@ce.sharif.edu
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
Email Gateway (Aug 18 2022 at 15:08):From: Brian Huffman <brianh@cs.pdx.edu>
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,
Email Gateway (Aug 18 2022 at 15:09):From: Christian Sternagel <christian.sternagel@uibk.ac.at>
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
Last updated: Apr 19 2024 at 16:20 UTC