# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1313567017 -7200
# Node ID 5d145fe77ec1c38ee2740bf5ac81a9cc5564ce3f
# Parent  5df574281b69d1cc1ae2cd3dd1858e80358b7ce1
a little tuning on the paper

diff -r 5df574281b69 -r 5d145fe77ec1 LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Tue Aug 16 17:48:09 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Wed Aug 17 09:43:37 2011 +0200
@@ -314,28 +314,32 @@
   The problem with introducing a new type in Isabelle/HOL is that in order to
   be useful, a reasoning infrastructure needs to be ``lifted'' from the
   underlying subset to the new type. This is usually a tricky and arduous
-  task. To ease it, we re-implemented in Isabelle/HOL \cite{KaliszykUrban11} the quotient package
-  described by Homeier \cite{Homeier05} for the HOL4 system. This package
-  allows us to lift definitions and theorems involving raw terms to
-  definitions and theorems involving alpha-equated terms. For example if we
-  define the free-variable function over raw lambda-terms
+  task. To ease it, we re-implemented in Isabelle/HOL \cite{KaliszykUrban11}
+  the quotient package described by Homeier \cite{Homeier05} for the HOL4
+  system. This package allows us to lift definitions and theorems involving
+  raw terms to definitions and theorems involving alpha-equated terms. For
+  example if we define the free-variable function over raw lambda-terms
 
-  \begin{center}
-  @{text "fv(x) \<equiv> {x}"}\\
-  @{text "fv(t\<^isub>1 t\<^isub>2) \<equiv> fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\hspace{8mm}
-  @{text "fv(\<lambda>x.t) \<equiv> fv(t) - {x}"}
-  \end{center}
+  \[
+  \mbox{\begin{tabular}{l@ {\hspace{1mm}}r@ {\hspace{1mm}}l}
+  @{text "fv(x)"}     & @{text "\<equiv>"} & @{text "{x}"}\\
+  @{text "fv(t\<^isub>1 t\<^isub>2)"} & @{text "\<equiv>"} & @{text "fv(t\<^isub>1) \<union> fv(t\<^isub>2)"}\\
+  @{text "fv(\<lambda>x.t)"}  & @{text "\<equiv>"} & @{text "fv(t) - {x}"}
+  \end{tabular}}
+  \]\smallskip
   
   \noindent
   then with the help of the quotient package we can obtain a function @{text "fv\<^sup>\<alpha>"}
   operating on quotients, or alpha-equivalence classes of lambda-terms. This
   lifted function is characterised by the equations
 
-  \begin{center}
-  @{text "fv\<^sup>\<alpha>(x) = {x}"}\hspace{8mm}
-  @{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2) = fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\hspace{8mm}
-  @{text "fv\<^sup>\<alpha>(\<lambda>x.t) = fv\<^sup>\<alpha>(t) - {x}"}
-  \end{center}
+  \[
+  \mbox{\begin{tabular}{l@ {\hspace{1mm}}r@ {\hspace{1mm}}l}
+  @{text "fv\<^sup>\<alpha>(x)"}     & @{text "="} & @{text "{x}"}\\
+  @{text "fv\<^sup>\<alpha>(t\<^isub>1 t\<^isub>2)"} & @{text "="} & @{text "fv\<^sup>\<alpha>(t\<^isub>1) \<union> fv\<^sup>\<alpha>(t\<^isub>2)"}\\
+  @{text "fv\<^sup>\<alpha>(\<lambda>x.t)"}  & @{text "="} & @{text "fv\<^sup>\<alpha>(t) - {x}"}
+  \end{tabular}}
+  \]\smallskip
 
   \noindent
   (Note that this means also the term-constructors for variables, applications