diff --git a/org.rodinp.handbook.feature/latex/reference-03.tex b/org.rodinp.handbook.feature/latex/reference-03.tex index 6eb20353c7b8f4e1edc323ae39b6550bac06c7a9..7fb1f3046be509c22c13d46535447034187ef3cc 100644 --- a/org.rodinp.handbook.feature/latex/reference-03.tex +++ b/org.rodinp.handbook.feature/latex/reference-03.tex @@ -184,8 +184,7 @@ The following reference subsections will have the form the form: \\[2em] \index{true!as predicate@as predicate ($\btrue$)}\index{false!as predicate@as predicate ($\bfalse$)} \index{$\btrue$ (true)} \index{$\bfalse$ (false)} -\hline -\vspace{5mm} + \begin{rrnames} $\btrue$ & \texttt{true} & True \\ $\bfalse$ & \texttt{false} & False \\ @@ -204,8 +203,7 @@ The following reference subsections will have the form the form: \\[2em] \index{conjunction@conjunction ($\land$)}\index{disjunction@disjunction ($\lor$)}\index{implication@implication ($\limp$)}\index{equivalence@equivalence ($\leqv$)}\index{negation@negation ($\lnot$)} \index{$\land$ (conjunction)}\index{$\lor$ (disjunction)}\index{$\limp$ (implication)}\index{$\leqv$ (equivalence)}\index{$\lnot$ (negation)} -\hline -\vspace{5mm} + \begin{rrnames} $\land$ & \texttt{\&} & Conjunction \\ @@ -261,8 +259,7 @@ The following reference subsections will have the form the form: \\[2em] \index{quantification!universal@universal ($\forall$)} \index{quantification!existential@existential ($\exists$)} -\hline -\vspace{5mm} + \begin{rrnames} $\forall$ & \texttt{!} & Universal quantification \\ $\exists$ & \texttt{\#} & Existential quantification \\ @@ -310,8 +307,7 @@ The following reference subsections will have the form the form: \\[2em] \subsubsection{Equality} \label{equality} \index{equality@equality ($=$)} -\hline -\vspace{5mm} + \begin{rrnames} $=$ & \texttt{=} & equality \\ $\neq$ & \texttt{/=} & inequality \\ @@ -333,8 +329,7 @@ The following reference subsections will have the form the form: \\[2em] \subsubsection{Membership} \label{membership} \index{membership@membership ($\in$)} -\hline -\vspace{5mm} + \begin{rrnames} $\in$ & \texttt{:} & set membership \\ $\not\in$ & \texttt{/:} & negated set membership \\ @@ -360,8 +355,7 @@ The following reference subsections will have the form the form: \\[2em] \index{boolean!the operator $\bool$} \index{true!as expression ($\True$)} \index{false!as expression ($\False$)} -\hline -\vspace{5mm} + \begin{rrnames} $\Bool$ & \texttt{BOOL} & Boolean values \\ $\True$ & \texttt{TRUE} & Boolean true \\ @@ -399,8 +393,7 @@ The following reference subsections will have the form the form: \\[2em] \subsubsection{Set comprehensions} \label{set_comprehensions} \index{set!comprehension set} -\hline -\vspace{5mm} + \begin{rrnames} $\{~\textit{ids}~\qdot~\predp~|~\expre~\}$ & \texttt{\{\textit{ids}.P|E\}} & Set comprehension \\ $\{~\expre~|~\predp~\}$ & \texttt{\{E|P\}} & Set comprehension (short form)\\ @@ -438,8 +431,7 @@ The following reference subsections will have the form the form: \\[2em] \subsubsection{Basic sets} \index{set!empty set@empty set ($\emptyset$)} \index{set!set extension} -\hline -\vspace{5mm} + \begin{rrnames} $\emptyset$ & \texttt{\{\}} & Empty set \\ $\{\textit{exprs}\}$ & \texttt{\{\textit{exprs}\}} & Set extension \\ @@ -466,8 +458,7 @@ The following reference subsections will have the form the form: \\[2em] \subsubsection{Subsets} \label{subsets} \index{subset@subset ($\subseteq,\subset$)} -\hline -\vspace{5mm} + \begin{rrnames} $\subseteq$ & \texttt{<:} & subset \\ $\not\subseteq$ & \texttt{/<:} & not a subset \\ @@ -501,8 +492,7 @@ The following reference subsections will have the form the form: \\[2em] \index{set!difference set@difference set ($\setminus$)} \index{set!set subtraction@set subtraction ($\setminus$)} \index{subtraction!of sets@of sets ($\setminus$)} -\hline -\vspace{5mm} + \begin{rrnames} $\bunion$ & \texttt{\mybackslash/} & Union \\ $\binter$ & \texttt{/\mybackslash} & Intersection \\ @@ -529,8 +519,7 @@ The following reference subsections will have the form the form: \\[2em] \begin{samepage} \subsubsection{Power sets} \index{set!power set@power set ($\pow$)} -\hline -\vspace{5mm} + \begin{rrnames} $\pow$ & \texttt{POW} & Power set \\ $\pow_1$ & \texttt{POW1} & Set of non-empty subsets \\ @@ -556,8 +545,7 @@ The following reference subsections will have the form the form: \\[2em] \index{set!finite} \index{set!cardinality@cardinality ($\card$)} \index{cardinality@cardinality ($\card$)} -\hline -\vspace{5mm} + \begin{rrnames} $\bfinite$ & \texttt{finite} & Finite set \\ $\card$ & \texttt{card} & Cardinality of a finite set \\ @@ -585,8 +573,7 @@ The following reference subsections will have the form the form: \\[2em] \label{partition} \index{partition} \index{set!partition} -\hline -\vspace{5mm} + \begin{rrnames} $\bpartition$ & \texttt{partition} & Partitions of a set \\ \end{rrnames} @@ -611,8 +598,7 @@ The following reference subsections will have the form the form: \\[2em] \subsubsection{Generalized union and intersection} \index{union!generalized union} \index{intersection!generalized intersection@generalized intersection ($\bunaryinter$)} -\hline -\vspace{5mm} + \begin{rrnames} $\bunaryunion$ & \texttt{union} & Generalized union \\ $\bunaryinter$ & \texttt{inter} & Generalized intersection \\ @@ -638,8 +624,7 @@ The following reference subsections will have the form the form: \\[2em] \subsubsection{Quantified union and intersection} \index{union!quantified union@quantified union ($\Union$)} \index{intersection!quantified intersection@quantified intersection ($\Inter$)} -\hline -\vspace{5mm} + \begin{rrnames} $\Union$ & \texttt{UNION} & Quantified union \\ $\Inter$ & \texttt{INTER} & Quantified intersection \\ @@ -683,8 +668,7 @@ The following reference subsections will have the form the form: \\[2em] \index{pair} \index{maplet@maplet ($\mapsto$)} \index{Cartesian product@Cartesian product ($\cprod$)} -\hline -\vspace{5mm} + \begin{rrnames} $\mapsto$ & \texttt{|->} & Pair \\ $\cprod$ & \texttt{**} & Cartesian product @@ -709,8 +693,7 @@ The following reference subsections will have the form the form: \\[2em] \begin{samepage} \subsubsection{Relations} \index{relation@relation ($\rel$,$\trel$,$\srel$,$\strel$)} -\hline -\vspace{5mm} + \begin{rrnames} $\rel$ & \texttt{<->} & Relations \\ $\trel$ & \texttt{<}\texttt{<->} & Total relations \\ @@ -747,8 +730,7 @@ The following reference subsections will have the form the form: \\[2em] \label{domain_and_range} \index{domain@domain ($\dom$)} \index{range@range ($\ran$)} -\hline -\vspace{5mm} + \begin{rrnames} $\dom$ & \texttt{dom} & Domain \\ $\ran$ & \texttt{ran} & Range \\ @@ -779,8 +761,7 @@ The following reference subsections will have the form the form: \\[2em] \index{domain subtraction@domain subtraction ($\domsub$)} \index{range restriction@range restriction ($\ranres$)} \index{range subtraction@range subtraction ($\ransub$)} -\hline -\vspace{5mm} + \begin{rrnames} $\domres$ & \texttt{<|} & Domain restriction\\ $\domsub$ & \texttt{<}\texttt{<|} & Domain subtraction\\ @@ -825,8 +806,7 @@ The following reference subsections will have the form the form: \\[2em] \index{relation!direct product ($\dprod$)} \index{inverse ($\mbox{}^{-1}$)} \index{relation!inverse ($\mbox{}^{-1}$)} -\hline -\vspace{5mm} + \begin{rrnames} $\fcomp$ & \texttt{;} & Relational forward composition\\ $\bcomp$ & \texttt{circ} & Relational backward composition\\ @@ -888,8 +868,7 @@ The following reference subsections will have the form the form: \\[2em] \label{relational_image} \index{relational image} \index{relation!image} -\hline -\vspace{5mm} + \begin{rrnames} $[\ldots]$ & \texttt{[}\ldots\texttt{]} & Relational image \end{rrnames} @@ -912,8 +891,7 @@ The following reference subsections will have the form the form: \\[2em] \index{identity relation@identity relation ($\id$)} \index{relation!identity ($\id$)} \index{projection@projection ($\prjone$,$\prjtwo$)} -\hline -\vspace{5mm} + \begin{rrnames} $\id$ & \texttt{id} & Identity relation \\ $\prjone$ & \texttt{prj1} & First projection \\ @@ -952,8 +930,7 @@ The following reference subsections will have the form the form: \\[2em] \index{injection@injection ($\pinj$,$\tinj$)} \index{surjection@surjection ($\psur$,$\tsur$)} \index{bijection@bijection ($\tbij$)} -\hline -\vspace{5mm} + \begin{rrnames} $\pfun$ & \texttt{+->} & Partial functions\\ $\tfun$ & \texttt{-->} & Total functions \\ @@ -1000,8 +977,7 @@ The following reference subsections will have the form the form: \\[2em] \subsubsection{Function application} \label{function_application} \index{function application} -\hline -\vspace{5mm} + \begin{rrnames} $(\ldots)$ & \texttt{(}\ldots\texttt{)} & Function application \end{rrnames} @@ -1023,8 +999,7 @@ The following reference subsections will have the form the form: \\[2em] \subsubsection{Lambda} \label{lambda} \index{lambda@lamba expression ($\lambda$)} -\hline -\vspace{5mm} + \begin{rrnames} $\lambda$ & \texttt{\%} & Lambda \end{rrnames} @@ -1070,8 +1045,7 @@ The following reference subsections will have the form the form: \\[2em] \subsubsection{Sets of numbers} \index{integer!as set@as set ($\intg$)} \index{natural numbers@natural numbers ($\nat$)} -\hline -\vspace{5mm} + \begin{rrnames} $\intg$ & \texttt{INT} & Integers \\ $\nat$ & \texttt{NAT} & Natural numbers, starting with 0 \\ @@ -1113,8 +1087,7 @@ The following reference subsections will have the form the form: \\[2em] \index{modulo@modulo ($\bmod$)} \index{reminder|see{modulo}} \index{exponentation@exponentation ($\expn$)} -\hline -\vspace{5mm} + \begin{rrnames} $+$ & \texttt{+} & Addition \\ $-$ & \texttt{-} & Subtraction or unary minus \\ @@ -1156,8 +1129,7 @@ The following reference subsections will have the form the form: \\[2em] \label{minimum_and_maximum} \index{minimum@minimum ($\min$)} \index{maximum@maximum ($\max$)} -\hline -\vspace{5mm} + \begin{rrnames} $\min$ & \texttt{min} & Minimum \\ $\max$ & \texttt{max} & Maximum @@ -1182,8 +1154,7 @@ The following reference subsections will have the form the form: \\[2em] \subsection{Typing} \label{typing} \index{oftype operator ($\boftype$)} -\hline -\vspace{5mm} + \begin{rrnames} $\boftype$ & \texttt{oftype} & of type \end{rrnames} @@ -1231,8 +1202,7 @@ The following reference subsections will have the form the form: \\[2em] \subsubsection{Deterministic Assignments} \label{deterministic_assignments} \index{assignment!deterministic ($\bcmeq$)} -\hline -\vspace{5mm} + \begin{rrnames} $\bcmeq$ & \texttt{:=} & deterministic assignment \end{rrnames} @@ -1276,8 +1246,7 @@ The following reference subsections will have the form the form: \\[2em] \index{assignment!become such@become such ($\bcmsuch$)} \index{become such@become such assignment ($\bcmsuch$)} \index{before-after predicate} -\hline -\vspace{5mm} + \begin{rrnames} $\bcmsuch$ & \texttt{:|} & non-deterministic assignment with a before-after-predicate \end{rrnames} @@ -1315,8 +1284,7 @@ The following reference subsections will have the form the form: \\[2em] \subsubsection{Non-deterministic assignment by sets} \index{assignment!become element of@become element of ($\bcmin$)} \index{become element of@become element of assignment ($\bcmin$)} -\hline -\vspace{5mm} + \begin{rrnames} $\bcmin$ & \texttt{::} & non-deterministic assignment of a set member \end{rrnames}