Fixes on Handbook

git-svn-id: svn://svn.code.sf.net/p/rodin-b-sharp/svn/trunk/Handbook@16185 1434b563-b632-4741-aa49-43a3a8374d2e

org.rodinp.handbook.feature/latex/faq.tex

@@ -106,7 +106,8 @@ Configuring Rodin on Linux can be tricky.  In particular, the pretty print view
 Add a property by appending the following code to your \textsf{eclipse/eclipse.ini} or \textsf{rodin/rodin.ini} file: 
 
 \begin{verbatim} 
-	-Dorg.eclipse.swt.browser.XULRunnerPath=/usr/lib/xulrunner/xulrunner-xxx 
+	-Dorg.eclipse.swt.browser.XULRunnerPath=
+	  /usr/lib/xulrunner/xulrunner-xxx 
 \end{verbatim} 
 
 \subsection{Some mathematical characters are wrong}

org.rodinp.handbook.feature/latex/makros.tex

@@ -12,7 +12,7 @@
 
 % for the print, we use an extra b&w directory
 \ifinprint
-\newcommand{\rodinimgdir}{bwimg}
+\newcommand{\rodinimgdir}{img}
 \else
 \newcommand{\rodinimgdir}{img}
 \fi
@@ -180,11 +180,7 @@
 }
 \fi
 
-\ifinprint
-\newenvironment{plugin-pror}{\begin{rodin-plugin}{bw/pror.png}{ProR Requirements}}{\end{rodin-plugin}}
-\else
 \newenvironment{plugin-pror}{\begin{rodin-plugin}{pror.png}{ProR Requirements}}{\end{rodin-plugin}}
-\fi
 
 % Marginpars are  cropped - this formats them nicely.
 \let\oldmarginpar\marginpar

org.rodinp.handbook.feature/latex/reference-01.tex

@@ -829,7 +829,7 @@ The auto-tactic automatically applies a combination (i.e. ordered list) of rewri
 
 The post-tactic is also a combination of rewrite tactics, inference tactics and external provers and is applied automatically after each interactive proof step. However, it can also be invoked manually by clicking on the \icon{rodin/broom_prover.png} button in the \textsf{Proof Control} view.
 
-Note that the post-tactic can be disabled quickly by clicking on the \textsf{rodin/expanded.png} button (marked with an A) of the \textsf{Proof Control} view (right upper corner) and then by deselecting the box next to the \textsf{Enable post-tactic} option (B) as shown in Figure \ref{fig_ref_01_proving_perspective12}. 
+Note that the post-tactic can be disabled quickly by clicking on the \icon{rodin/expanded.png} button (marked with an A) of the \textsf{Proof Control} view (right upper corner) and then by deselecting the box next to the \textsf{Enable post-tactic} option (B) as shown in Figure \ref{fig_ref_01_proving_perspective12}. 
 
 \begin{figure}[!ht]
 \begin{center}

org.rodinp.handbook.feature/latex/reference-02.tex

@@ -283,7 +283,8 @@ All variables to which no new value is assigned keep the same value in new and o
 \index{before-after predicate}
 We now define the before-after-predicate $\concbeforeafter$ of the actions together.
 Let $Q_1,\ldots,Q_n$ be the before-after-predicate of the event's assignments. 
-Let $x_1,\ldots,x_k$ be the variables that are assigned by any action of the event.
+Let $x_1,\ldots,$ $x_k$ % broke formular for print
+be the variables that are assigned by any action of the event.
 Let $y_1,\ldots,y_l$ be the variables of the concrete machine that are \emph{not} modified by any of 
  the event's actions (i.e. $\concvariables = x_1,\ldots,x_k,y_1,\ldots,y_l$).
 Then the before-after-predicate of the concrete event is 
@@ -675,7 +676,7 @@ a reference to the relevant reference section is provided.
 \index{FIS (feasibility proof obligation)}
 \index{INV (invariant proof obligation)}
 \index{GRD (guard-strengthening proof obligation)}
-\index{MRG (guard-strengthening (merge) proof obligation)}
+\index{MRG (guard-strengthening (merge) pr\-oof obligation)}
 \index{SIM (simulation proof obligation)}
 \index{EQL (equality of preserved variable proof obligation)}
 \index{WWD (well-definedness of witness proof obligation)}

org.rodinp.handbook.feature/latex/rodin-doc.tex

 \ifdefined\isinprint
 \documentclass[twoside,10pt]{book}
 \usepackage[twoside,paperwidth=155.93mm,paperheight=233.89mm,hmargin={15mm,15mm},vmargin={20mm,20mm},bindingoffset=5mm]{geometry}
+\usepackage[hyphens]{url} 
 \usepackage[colorlinks=false,
             pdfborder={0 0 0}
 	        pdftex,
             plainpages=false,
-            pdfauthor={Michael Jastram (Ed.)},
+            pdfauthor={Michael Jastram (Editor)},
             pdftitle={Rodin User's Handbook},
             pdfsubject={Rodin is a platform for Event-B based formal modelling},
             pdfkeywords={Rodin, Event-B},
@@ -14,6 +15,7 @@
 \else
 \documentclass[12pt]{book}
 \usepackage[left=2.5cm,top=3cm,right=2.5cm,bottom=3cm]{geometry}
+\usepackage[hyphens]{url} 
 \usepackage[colorlinks=true,
 	        pdftex,
             plainpages=false,
@@ -64,7 +66,7 @@ Handbook $ $Rev$ $ \\
 {\titledimsubtext\selectfont \textbf{\textsf{Covers Rodin v.\versionnr}}}
 
 \vspace*{\titlesecdistance}
-{\titledimsubtext\selectfont \textsf{Michael Jastram (Ed.)}}
+{\titledimsubtext\selectfont \textsf{Michael Jastram (Editor)}}
 
 \vspace*{\titlesubtitledistance}
 {\titledimsubtext\selectfont \textsf{Foreword by Prof. Michael Butler}}
@@ -91,7 +93,7 @@ Handbook $ $Rev$ $ \\
 \vspace*{\fill}
 \noindent\textbf{Rodin User's Handbook}\\
 ~\\
-\noindent\copyright Formal Mind Gmbh 2013\\
+\noindent\copyright Formal Mind Gmbh 2014\\
 This work, except the cover image, is licensed under the Creative Commons Attribution-ShareAlike 3.0 Unported License. To view a copy of this license, visit \href{http://creativecommons.org/licenses/by-sa/3.0/}{creative\-com\-mons.org/\-licenses/\-by-sa/3.0/} or send a letter to Creative Commons, 444 Castro Street, Suite 900, Mountain View, California, 94041, USA.\\
 The cover image of a Rodin statue was created by Miikka Skaffari.
 It is licensed under a Creative Commons Attribution-NonCommercial 3.0 Unported License.  To view a copy of this license, visit \href{http://creativecommons.org/licenses/by-sa/3.0/}{creative\-com\-mons.org/\-licenses/\-by-sa/3.0/} or send a letter to Creative Commons, 444 Castro Street, Suite 900, Mountain View, California, 94041, USA.

org.rodinp.handbook.feature/latex/tutorial-04.tex

@@ -140,7 +140,7 @@ constants and state that $apples \subseteq FRUITS$ and $oranges \subseteq FRUITS
 If apples and oranges are all fruits we want to model, we can assume $apples \cup oranges = FRUITS$
 and if no fruit is both an apple and orange we can write $apples \cap oranges = \emptyset$.
 A shorter way to express this is to say that apples and oranges constitute a
-partition of the fruits: $partition(FRUITS,apples,oranges)$.
+partition of the fruits: $partition(FRUITS,$ $apples,$ $oranges)$. % broke formula for print version
 In general, we can use the partition operator to express that a set $S$ is partitioned by the
 sets $s_1,\ldots,s_n$ with $partition(S,s_1,\ldots,s_n)$.  We use partitions in Section~\ref{tut_modelling_persons}.
 

org.rodinp.handbook.feature/latex/tutorial-06.tex

@@ -172,7 +172,8 @@ concrete guards can be used as hypotheses in the proof.
 
 The second condition, that the gluing invariant remains true, is just a more general case of the proof obligation which ensures 
 that an event does not violate the invariant. So the proof obligation's label is again 
-\eventbpo{concrete\_event/concrete\_invariant/INV}. The goal is to prove that the invariant of the concrete machine is valid when each occurrence of a modified variable is replaced by its new value.
+\eventbpo{con\-crete\_event/con\-crete\_invariant/INV}.
+The goal is to prove that the invariant of the concrete machine is valid when each occurrence of a modified variable is replaced by its new value.
 The hypotheses we use are:
 \begin{itemize}
 \item We assume that the invariant of both the concrete and abstract machines were valid before the event occurred.

org.rodinp.handbook.feature/latex/tutorial-07.tex

@@ -130,7 +130,7 @@ Next, we will create a gluing invariant (\ref{abstract_machine}) that associates
 \end{description}
 }
 
-In its current state, this gluing invariant can be violated: if the event \textsf{set\_peds\_go} is triggered, for instance, the variable \textsf{peds\_go} will change but \textsf{peds\_colour} will not.  We expect that this will result in undischarged proof obligations (\ref{generated_proof_obligations}).  We can check this by expanding the machine in the Event-B Explorer.  Indeed, we now see two undischarged proof obligations (compare with Figure \ref{fig_tut_07_undischarged}).
+In its current state, this gluing invariant can be violated: if the event \textsf{set\_peds\_go} is triggered, for instance, the variable \textsf{peds\_go} will change but \textsf{peds\_\-colour} will not.  We expect that this will result in undischarged proof obligations (\ref{generated_proof_obligations}).  We can check this by expanding the machine in the Event-B Explorer.  Indeed, we now see two undischarged proof obligations (compare with Figure \ref{fig_tut_07_undischarged}).
 
 \begin{figure}[!ht]
 \begin{center}