Improvements to proof generation from transformation trace. Better handling of unfold. First version of handling proofs of postcondition refinments: currently only works for simple cases.
Improvements to proof generation from transformation trace.
Better handling of unfold.
First version of handling proofs of postcondition refinments:
currently only works for simple cases.


git-svn-id: 9ecf60ce9baff443e30a0472d3fd222fcb8117cf@7904 7b97033b-253e-4a5c-9b07-e25f9089a9fd

KestrelInstitute/Specware,KestrelInstitute/Specware,KestrelInstitute/Specware,KestrelInstitute/Specware,KestrelInstitute/Specware