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 of Isabelle.
	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 MHonArc.