]> matita.cs.unibo.it Git - helm.git/commitdiff
more style fixes
authorEnrico Tassi <enrico.tassi@inria.fr>
Thu, 2 Feb 2006 11:44:44 +0000 (11:44 +0000)
committerEnrico Tassi <enrico.tassi@inria.fr>
Thu, 2 Feb 2006 11:44:44 +0000 (11:44 +0000)
helm/papers/system_T/t.tex

index 42b937bf2a1e9223f4386cdd267dbf86457aabcc..a3f08cd5a66fd43832cfa49f469e0381817ab280 100644 (file)
@@ -179,23 +179,24 @@ informative part of the algorithms.
 {\bf Inference Rules}
 
 say that ax:AX refers to the previous Axioms list...
-\begin{table}[!h]
-\hrule\vspace{0.1cm}
-\begin{tabular}{p{0.34\textwidth}r}
-  $\Gamma, x:A, \Delta \vdash x:A$ & $(Proj)$\\
-  $\Gamma \vdash ax : AX$ & $(Const)$\\
-  $\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q}$ & 
-    $(\to_i)$\\
-  $\frac{\Gamma \vdash M: A \to Q \hspace{0.5cm}\Gamma \vdash N: A}
-        {\Gamma \vdash M N: Q}$ & $(\to_e)$\\
-  $\frac{\Gamma \vdash M:P}{\Gamma \vdash \lambda x:\N.M: \forall x.P}(*)$ &
-    $(\forall_i)$\\
-  $\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}$ &
-    $(\forall_e)$
-\end{tabular}\vspace{0.1cm}
-\hrule
-\caption{\label{tab:HArules}Inference rules}
-\end{table}{lr}
+%\begin{table}[!h]
+%\hrule\vspace{0.1cm}
+%\begin{tabular}{p{0.34\textwidth}r}
+
+  $$\Gamma, x:A, \Delta \vdash x:A ~~~ (Proj)$$
+  $$ \Gamma \vdash ax : AX~~~ (Const)$$
+  $$\frac{\Gamma,x:A \vdash M:Q}{\Gamma \vdash \lambda x:A.M: A \to Q} ~~~ (\to_i)$$
+  $$\frac{\Gamma \vdash M: A \to Q \hspace{0.5cm}\Gamma \vdash N: A}
+        {\Gamma \vdash M N: Q} ~~~ (\to_e)$$
+  $$\frac{\Gamma \vdash M:P}{\Gamma \vdash \lambda x:\N.M: \forall x.P}(*) ~~~
+    (\forall_i)$$
+  $$\frac{\Gamma \vdash M :\forall x.P}{\Gamma \vdash M t: P[t/x]}
+     ~~~ (\forall_e)$$
+    
+%\end{tabular}\vspace{0.1cm}
+%\hrule
+%\caption{\label{tab:HArules}Inference rules}
+%\end{table}{lr}
 
 %\[ 
 %   (\land_i)\frac{\Gamma \vdash M:A \hspace{1cm}\Gamma \vdash N:B}