Re: [isabelle] apply a rewriting-lemma only once



Hi Roger,

> I mean i only want to rewrite the "a" with "a+1" only once..cause by default it will rewrite forever and i dont want that.

try the 'subst' method:

  apply (subst your_theorem)

See also this recent thread:
<http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/12006>

Cheers
Lars




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