# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1308620365 -32400
# Node ID 3c981d009fe51b963cf8263fdb8ce350f56e08a9
# Parent  ac42c37ffbde1fa6caa54bdbd86bcdc4ddf666e3# Parent  c24f86c595ca4e2ead3b23a5770998654c198005
merge

diff -r ac42c37ffbde -r 3c981d009fe5 ESOP-Paper/Paper.thy
--- a/ESOP-Paper/Paper.thy	Mon Jun 20 20:09:51 2011 +0900
+++ b/ESOP-Paper/Paper.thy	Tue Jun 21 10:39:25 2011 +0900
@@ -1715,7 +1715,7 @@
   any bound atoms. In Ott, in contrast, the user may 
   define @{text "bn"}$_{1..m}$ so that they return bound
   atoms and in this case the third implication is \emph{not} true. A 
-  result is that the lifing of the corresponding binding functions in Ott to $\alpha$-equated
+  result is that the lifting of the corresponding binding functions in Ott to $\alpha$-equated
   terms is impossible.
 
   Having established respectfulness for the raw term-constructors, the