Adjusted the proof obligations so that undischarged proof obligations produce a verification failure.
fixed the unit-b style sheet
Improved the automatic compilation program
Fixed the propagation of imports along the refinement order.
Added an example with more elaborate refinements. To be extended.