[isabelle] Question to "lemmas" - instruction



Hello,

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?


Bye,
Thomas





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