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

No Subject




I am working on some strategies, and I have found that even if a strategy
is changed a previously finished proof is still accepted.

Example:

a is proven using strategy s
s is changed
if using C-c C-p t to re-prove the theory, the old proof of a is still
assumed correct, even if s might not work on a anymore.

Is there a way to force PVS to re-prove all the lemmas in a theory, other
than doing each of them individually?

Thanks,
Hanne
---------------------------------------------------------
Hanne Gottliebsen		    Office P337
Dept. of Computer Science	    Ph: +44 1334 46 3265
University of St Andrews	    hago@dcs.st-and.ac.uk
                   - Who moved the stone?
---------------------------------------------------------