Re: [isabelle] Question to "lemmas" - instruction
You can use
lemmas a_prime = two_prime [unfolded a_def[symmetric]]
Thomas Goethel wrote:
If I have a have a lemma like
lemma two_prime: "isPrime 2"
and a definition
constdefs a:: nat
"a == 2"
then it is of course possible to prove "isPrime a".
This prove is very trivial, so I would like to use the "lemmas" - instruction
lemmas a_prime = two_prime [...]
Does a method exist to reach this goal?
This archive was generated by a fusion of
Pipermail (Mailman edition) and