Skip to content
Snippets Groups Projects
Commit 2bc13f57 authored by Daniel Plagge's avatar Daniel Plagge
Browse files

green check -> green mark

git-svn-id: svn://svn.code.sf.net/p/rodin-b-sharp/svn/trunk/Handbook@15966 1434b563-b632-4741-aa49-43a3a8374d2e
parent f8108fa1
No related branches found
No related tags found
No related merge requests found
...@@ -362,7 +362,7 @@ The \texttt{Proving Perspective} contains three new important views: ...@@ -362,7 +362,7 @@ The \texttt{Proving Perspective} contains three new important views:
\item[Goal View (\ref{goal_view})] This window shows what needs to be proved at the current position inside the proof tree. \item[Goal View (\ref{goal_view})] This window shows what needs to be proved at the current position inside the proof tree.
\end{description} \end{description}
Expand the \texttt{Celebrity\_1} machine in the \textsf{Event-B Explorer}. Then expand the \textsf{Proof Obligations} section. We can see that the auto prover (\ref{auto_prover}) did quite a good job. Only three proofs have not been completed\footnote{Interestingly enough, this number can vary: Provers can be configured in the preferences and changes there can have an impact on the ability to automatically discharge proofs. In addition, all provers have timeouts. On a slow machine, some proof obligations may not be discharged whereas on a faster machine with the same timeout they would be discharged.} (a completed proof is indicated by a green check \icon{rodin/discharged.png}). Expand the \texttt{Celebrity\_1} machine in the \textsf{Event-B Explorer}. Then expand the \textsf{Proof Obligations} section. We can see that the auto prover (\ref{auto_prover}) did quite a good job. Only three proofs have not been completed\footnote{Interestingly enough, this number can vary: Provers can be configured in the preferences and changes there can have an impact on the ability to automatically discharge proofs. In addition, all provers have timeouts. On a slow machine, some proof obligations may not be discharged whereas on a faster machine with the same timeout they would be discharged.} (a completed proof is indicated by a green mark \icon{rodin/discharged.png}).
%Except for the last one of them, all of them could be proved with a different external prover, but in order to learn a few new techniques, we will prove them with the so called ``p0 prover'' (\ref{p0_prover}). The p0 prover uses all selected hypotheses (the ones in Selected Hypotheses View). %Except for the last one of them, all of them could be proved with a different external prover, but in order to learn a few new techniques, we will prove them with the so called ``p0 prover'' (\ref{p0_prover}). The p0 prover uses all selected hypotheses (the ones in Selected Hypotheses View).
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment