From 08a774ecbf6394f5004069318fd326f98244f5c4 Mon Sep 17 00:00:00 2001 From: Daniel Plagge <plagge@cs.uni-duesseldorf.de> Date: Thu, 10 Oct 2013 15:55:29 +0000 Subject: [PATCH] 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 --- org.rodinp.handbook.feature/latex/tutorial-08.tex | 2 -- 1 file changed, 2 deletions(-) diff --git a/org.rodinp.handbook.feature/latex/tutorial-08.tex b/org.rodinp.handbook.feature/latex/tutorial-08.tex index 8a95ba0..6e300a6 100644 --- a/org.rodinp.handbook.feature/latex/tutorial-08.tex +++ b/org.rodinp.handbook.feature/latex/tutorial-08.tex @@ -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$)}, -- GitLab