# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1269345822 -3600
# Node ID c8c9b3b7189a0f169de744be141967498cb5937c
# Parent  091f373baae9e75f773d58f12f921e4ac1d3b6e6
tuned paper

diff -r 091f373baae9 -r c8c9b3b7189a Paper/Paper.thy
--- a/Paper/Paper.thy	Tue Mar 23 11:52:55 2010 +0100
+++ b/Paper/Paper.thy	Tue Mar 23 13:03:42 2010 +0100
@@ -580,20 +580,25 @@
   lambda-terms and type-schemes use them:
 
   \begin{center}
-  \begin{tabular}{cc}
-  \begin{tabular}{l}
-  \isacommand{nominal\_datatype} lam =\\
-  \hspace{5mm}Var\;{\it name}\\
-  \hspace{5mm}App\;{\it lam}\;{\it lam}\\
-  \hspace{5mm}Lam\;{\it x::name}\;{\it t::lam}\;
-  \isacommand{bind} {\it x} \isacommand{in} {\it t}\\
+  \begin{tabular}{@ {}cc@ {}}
+  \begin{tabular}{@ {}l@ {\hspace{-1mm}}}
+  \isacommand{nominal\_datatype} {\it lam} =\\
+  \hspace{5mm}\phantom{$\mid$} Var\;{\it name}\\
+  \hspace{5mm}$\mid$ App\;{\it lam}\;{\it lam}\\
+  \hspace{5mm}$\mid$ Lam\;{\it x::name}\;{\it t::lam}\\
+  \hspace{22mm}\isacommand{bind} {\it x} \isacommand{in} {\it t}\\
   \end{tabular} &
-  \begin{tabular}{l}
-  foo
+  \begin{tabular}{@ {}l@ {}}
+  \isacommand{nominal\_datatype} {\it ty} =\\
+  \hspace{5mm}\phantom{$\mid$} TVar\;{\it name}\\
+  \hspace{5mm}$\mid$ TFun\;{\it ty}\;{\it ty}\\
+  \isacommand{and} {\it S} = All\;{\it xs::(name fset)}\;{\it T::ty}\\
+  \hspace{27mm}\isacommand{bind} {\it xs} \isacommand{in} {\it T}\\
   \end{tabular}
   \end{tabular}
   \end{center}
 
+  \noindent
   A specification of a term-calculus in Nominal Isabell is very similar to 
   the usual datatype definition of Isabelle/HOL: