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

How to rewrite all instances at once



Tad Taylor writes:
 > I seem to be struggling with the syntax of prover commands again.  I'd
 > often like to rewrite all instances of a function in both the
 > antecedent and consequent, however I can only get rewrite to do one at
 > a time.  I'm pretty sure you can do this.  What's the command syntax
 > to do this?  Thanks,

It sounds like you want to use (expand "<function-name>")

-- 
-- Paul S. Miner                | email: p.s.miner@larc.nasa.gov
-- 1 South Wright St. / MS 130  |   fax: (757) 864-4234
-- NASA Langley Research Center | phone: (757) 864-6201
-- Hampton, Virginia 23681-0001 |