diff -r 9c968d0de9a0 -r 2ce98ee39990 inferences.tex
--- a/inferences.tex	Sat Oct 04 12:46:04 2014 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,91 +0,0 @@
-\documentclass{article}
-\usepackage{charter}
-\usepackage{proof}
-
-\begin{document}
-
-\section*{Inference Rules}
-
-\begin{enumerate}
-\item Frequently used inference rules:
-
-\begin{center}
-\mbox{\infer{F,\Gamma \vdash F}{}}\medskip
-
-\mbox{\infer{\Gamma \vdash F_2}
-            {\Gamma \vdash F_1 \Rightarrow F_2 & \Gamma \vdash F_1}}
-\hspace{10mm}
-\mbox{\infer{\Gamma \vdash F_1 \Rightarrow F_2}
-            {F_1, \Gamma \vdash F_2}}\medskip
-
-\mbox{\infer{\Gamma \vdash P \;\textit{says}\; F}
-            {\Gamma \vdash F}}
-\hspace{10mm}
-\mbox{\infer[\star]{\Gamma \vdash F}
-            {\Gamma \vdash P \;\textit{controls}\; F & \Gamma \vdash P
-              \;\textit{says}\; F}}\medskip
-
-\mbox{\infer{\Gamma \vdash P \;\textit{says}\;F_2}
-            {\Gamma \vdash P \;\textit{says}\; (F_1 \Rightarrow F_2) & 
-             \Gamma \vdash P \;\textit{says}\;F_1}}\medskip
-
-\mbox{\infer{\Gamma \vdash F[x := t]}
-            {\Gamma \vdash \forall x. F}}\medskip
-
-\mbox{\infer{\Gamma \vdash F_1 \wedge F_2}
-            {\Gamma \vdash F_1 & \Gamma \vdash F_2}}
-\hspace{10mm}
-\mbox{\infer{\Gamma \vdash F_1}
-            {\Gamma \vdash F_1 \wedge F_2}}
-\hspace{10mm}
-\mbox{\infer{\Gamma \vdash F_2}
-            {\Gamma \vdash F_1 \wedge F_2}}\medskip
-
-\mbox{\infer[\star]{\Gamma \vdash Q\;\textit{says}\; F}{\Gamma \vdash P\mapsto Q &
-    \Gamma \vdash P\;\textit{says}\; F}}
-\end{center}
-
-\item Less frequently used inference rules:
-
-\begin{center}
-\mbox{\infer{\Gamma \vdash slev(P) < slev(Q)}
-            {\Gamma \vdash slev(P) = l_1 & \Gamma \vdash slev(Q) = l_2 &
-              \Gamma \vdash l_1 < l_2}}\medskip
-
-\mbox{\infer{\Gamma \vdash slev(P) = slev(Q)}
-            {\Gamma \vdash slev(P) = l & \Gamma \vdash slev(Q) = l}}\medskip
-
-\mbox{\infer{\Gamma \vdash l_1 < l_3}
-            {\Gamma \vdash l_1 < l_2 & \Gamma \vdash l_2 < l_3}}\medskip
-
-\mbox{\infer[\star]{\Gamma \vdash P \mapsto R}{\Gamma \vdash P\mapsto Q & \Gamma
-    \vdash Q \mapsto R}}\medskip
-
-
-\mbox{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_1}}
-\hspace{5mm}
-\mbox{\infer{\Gamma \vdash F_1 \vee F_2}{\Gamma \vdash F_2}}
-\hspace{5mm}
-\mbox{\infer{\Gamma \vdash F_3}{\Gamma \vdash F_1 \vee F_2 & F_1, \Gamma
-    \vdash F_3 & F_2, \Gamma \vdash F_3}}\medskip
-
-\mbox{\infer[c\;\mbox{must be a fresh variable}]{\Gamma \vdash \forall
-    x. F}{\Gamma \vdash F[x := c]}}\medskip
-
-\mbox{\infer{\Gamma \vdash \textit{true}}{}}\medskip
-
-\mbox{\infer[\star]{\Gamma \vdash P\;\textit{controls}\; F}{\Gamma \vdash P\mapsto Q
-    & \Gamma \vdash Q\;\textit{controls} F}}
-
-
-\end{center}
-\end{enumerate}
-
-
-$\star$ derived rules
-\end{document}
-
-%%% Local Variables: 
-%%% mode: latex
-%%% TeX-master: t
-%%% End: