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:


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