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

removed not needed pagebreaks

git-svn-id: svn://svn.code.sf.net/p/rodin-b-sharp/svn/trunk/Handbook@15977 1434b563-b632-4741-aa49-43a3a8374d2e
parent f1269c9d
No related branches found
No related tags found
No related merge requests found
......@@ -9,7 +9,6 @@
In this section, we will work with the model of the so-called celebrity problem.
%\ifinprint\pagebreak\fi %TODO: remove this
\warning{We are using a new model instead of the traffic light because it provides us with some proofs where manual interaction is necessary.}
In the setting for this problem, we have a ``knows'' relation between persons.
......@@ -395,7 +394,6 @@ The event's action assigns the new value $Q\setminus \{x\}$ to $Q$.
Because we know that invariant $c\in Q$ was valid before the assignment,
it is sufficient to prove that we do not remove $c$ from $Q$, i.e. \textsf{$x \neq c$}. Type this into the \textsf{Proof Control View} (\ref{proof_control_view}) and press the \textsf{\icon{rodin/ah_prover.png} button}.
\ifinprint\pagebreak\fi %TODO: remove this
\info{In order to undo a step, click on a node in the \texttt{Proof Tree View} and click on the \icon{rodin/pn_prover.png} button in the \texttt{Proof Control View} or open the context menu of a node and select \texttt{Prune}.}
Take a look at the Proof Tree View. The root node should now be labelled with \texttt{ah ($x\neq c$)},
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment