X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?a=blobdiff_plain;f=article.tex;h=198ced4b05e9700e0a4e5ac41b07e0e8dad1c631;hb=23129e4ede4f93a172b3eab8e51144f2488af972;hp=052b28b00b62819dc574bb770256bc42a7318355;hpb=652eb22f1325067110e21c4c90eb3f2533967042;p=topbloke-formulae.git diff --git a/article.tex b/article.tex index 052b28b..198ced4 100644 --- a/article.tex +++ b/article.tex @@ -26,7 +26,7 @@ \newcommand{\has}{\sqsupseteq} \newcommand{\isin}{\sqsubseteq} -\newcommand{\nothaspatch}{\mathrel{\,\!\not\relax\haspatch}} +\newcommand{\nothaspatch}{\mathrel{\,\not\!\not\relax\haspatch}} \newcommand{\notpatchisin}{\mathrel{\,\not\!\not\relax\patchisin}} \newcommand{\haspatch}{\sqSupset} \newcommand{\patchisin}{\sqSubset} @@ -46,6 +46,10 @@ \newcommand{\py}{\pay{P}} \newcommand{\pn}{\pan{P}} +\newcommand{\pc}{\pa{C}} +\newcommand{\pcy}{\pay{C}} +\newcommand{\pcn}{\pan{C}} + \newcommand{\pl}{\pa{L}} \newcommand{\ply}{\pay{L}} \newcommand{\pln}{\pan{L}} @@ -82,9 +86,11 @@ \newcommand{\patch}{{\mathcal P}} \newcommand{\base}{{\mathcal B}} +\newcommand{\depsreq}{{\mathcal D}} \newcommand{\patchof}[1]{\patch ( #1 ) } \newcommand{\baseof}[1]{\base ( #1 ) } +\newcommand{\depsreqof}[1]{\depsreq ( #1 ) } \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} } \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} } @@ -97,6 +103,13 @@ {\hbox{\normalsize$\forall$}}% {\hbox{\scriptsize$\forall$}}}% } +\newcommand{\bigexists}{% + \mathop{\mathchoice% + {\hbox{\huge$\exists$}}% + {\hbox{\Large$\exists$}}% + {\hbox{\normalsize$\exists$}}% + {\hbox{\scriptsize$\exists$}}}% +} \newcommand{\Largeexists}{\mathop{\hbox{\Large$\exists$}}} \newcommand{\Largenexists}{\mathop{\hbox{\Large$\nexists$}}} @@ -113,6 +126,8 @@ \begin{document} +\chapter{Data model} + \input{notation.tex} \input{invariants.tex} \input{lemmas.tex} @@ -124,4 +139,8 @@ \input{anticommit.tex} \input{merge.tex} +\chapter{Merge strategy} + +\input{strategy.tex} + \end{document}