[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] Body of lemmas



Is it possible to access the body of a particlar lemma from a
strategy?  My goal is to write a strategy where I can invoke 
(strategy "lemma") in a manner similar to (rewrite "lemma"). 

Thank you,

    Erika