# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1334067532 -3600
# Node ID 990f066609c93f211af993e0fe3a336515affd1e
# Parent  fde87a11377cb78c0907e30f7c1e717fdf52a6f8
some slight polishing on the LMCS paper

diff -r fde87a11377c -r 990f066609c9 LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Wed Apr 04 06:20:16 2012 +0100
+++ b/LMCS-Paper/Paper.thy	Tue Apr 10 15:18:52 2012 +0100
@@ -125,21 +125,23 @@
   \]\smallskip
 
   \noindent
-  which relates a type-scheme with a list of type-variables and a type. The point of this
-  definition is: given a type-scheme @{text S}, how to get access to the bound type-variables 
-  and the type-part of this type-scheme? The unbinding relation gives an answer, though in general 
+  Its purpose is to relate a type-scheme with a list of type-variables and a type. It is used to
+  address the following problem:
+  Given a type-scheme @{text S}, how does one get access to the bound type-variables 
+  and the type-part of @{text S}? The unbinding relation gives an answer, though in general 
   we will only get access to some type-variables and some type that are  
   ``alpha-equivalent'' to @{text S}. This is because unbinding is a relation; it cannot be a function
   for alpha-equated type-schemes. 
   Still, with this 
-  definition in place we can formally define when a type is an instance of a type-scheme as
+  definition in place we can formally define when a type is an instance of a type-scheme 
+  as follows:
 
   \[
   @{text "T \<prec> S \<equiv> \<exists>xs T' \<sigma>. S \<hookrightarrow> (xs, T') \<and> dom \<sigma> = set xs \<and> \<sigma>(T') = T"}
   \]\smallskip
   
   \noindent
-  meaning there exists a list of type-variables @{text xs} and a type @{text T'} to which
+  This means there exists a list of type-variables @{text xs} and a type @{text T'} to which
   the type-scheme @{text S} unbinds, and there exists a substitution whose domain is
   @{text xs} (seen as set) such that @{text "\<sigma>(T') = T"}.
   The problem with this definition is that we cannot follow the usual proofs