This option is invoked from the
Provers Environment
and is applicable
to all
machines,
refinements,
and
implementations,
which currently
have undischarged proof obligations; a list of such obligations is
displayed in the
Display Area
in the form `operation.number', together with information on each proved level.
A full on-line help listing is available
in the Contents Page
Also available in the form of a complete
Index.
© B-Core
(UK) Limited, Last updated: 22 Feb 2002