[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?
---------------------------------------------------------