X-Git-Url: http://www.chiark.greenend.org.uk/ucgi/~ian/git?p=topbloke-formulae.git;a=blobdiff_plain;f=article.tex;h=8ecdbc394a04fde93eadc52bda85d26199fd8174;hp=740a2bc406c37588e03e7e676611d57ce7c8a8d7;hb=0853ae723fa4d36f9033ddef7ca3871f8cec6d83;hpb=883050622af6e64f7a035aba410a2983c639a393 diff --git a/article.tex b/article.tex index 740a2bc..8ecdbc3 100644 --- a/article.tex +++ b/article.tex @@ -65,8 +65,8 @@ %\newcommand{\hasparents}{\underaccent{1}{>}} %\newcommand{\hasparents}{{% % \declareslashed{}{_{_1}}{0}{-0.8}{>}\slashed{>}}} -\newcommand{\hasparents}{>_{\mkern-7.0mu _1}} -\newcommand{\areparents}{<_{\mkern-14.0mu _1\mkern+5.0mu}} +\newcommand{\hasparents}{>_{\mkern-7.0mu _{1:}}} +\newcommand{\areparents}{<_{\mkern-14.0mu _{1:}\mkern+5.0mu}} \renewcommand{\implies}{\Rightarrow} \renewcommand{\equiv}{\Leftrightarrow} @@ -95,6 +95,25 @@ \newcommand{\eqntag}[2]{ #2 \tag*{\mbox{#1}} } \newcommand{\eqn}[2]{ #2 \tag*{\mbox{\bf #1}} } +\newcommand{\hasdirdep}{\succ_{\mkern-7.0mu _1}} +\newcommand{\hasdep}{\succ} +\newcommand{\isdep}{\prec} + +\newcommand{\grefz}{ T^0 } +\newcommand{\grefc}{ T } +\newcommand{\grefu}{ T' } +\newcommand{\greff}{ T^* } + +\newcommand{\grefza}[1]{ \grefz_{#1} } +\newcommand{\grefca}[1]{ \grefc_{#1} } +\newcommand{\grefua}[1]{ \grefu_{#1} } +\newcommand{\greffa}[1]{ \greff_{#1} } + +\newcommand{\grefzc}{ \grefza \pc } +\newcommand{\grefcc}{ \grefca \pc } +\newcommand{\grefuc}{ \grefua \pc } +\newcommand{\greffc}{ \greffa \pc } + %\newcommand{\bigforall}{\mathop{\hbox{\huge$\forall$}}} \newcommand{\bigforall}{% \mathop{\mathchoice% @@ -126,6 +145,8 @@ \begin{document} +\chapter{Data model} + \input{notation.tex} \input{invariants.tex} \input{lemmas.tex} @@ -136,6 +157,9 @@ \input{create-tip.tex} \input{anticommit.tex} \input{merge.tex} + +\chapter{Merge strategy} + \input{strategy.tex} \end{document}