# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1316599683 -7200
# Node ID 1447c135080c26170e9515a6e0b568c0ef2c0d10
# Parent  dc4b779f9338b3a492cad95dd8114b1b26c326ee
some minor polishing

diff -r dc4b779f9338 -r 1447c135080c LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Wed Sep 21 12:01:34 2011 +0200
+++ b/LMCS-Paper/Paper.thy	Wed Sep 21 12:08:03 2011 +0200
@@ -2154,7 +2154,7 @@
   for @{text "c"} (third line); for @{text "Let_pat\<^sup>\<alpha>"} we can assume
   all bound atoms from an assignment are fresh for @{text "c"} (fourth
   line). In order to see how an instantiation for @{text "c"} in the
-  conclusion `controls' the premises, you have to take into account that
+  conclusion `controls' the premises, one has to take into account that
   Isabelle/HOL is a typed logic. That means if @{text "c"} is instantiated
   with a pair, for example, then this type-constraint will be propagated to
   the premises. The main point is that if @{text "c"} is instantiated