# HG changeset patch
# User Cezary Kaliszyk <kaliszyk@in.tum.de>
# Date 1308620263 -32400
# Node ID c24f86c595ca4e2ead3b23a5770998654c198005
# Parent  06d91b7b575609665e6616a2b054bcde3512126c
spelling

diff -r 06d91b7b5756 -r c24f86c595ca ESOP-Paper/Paper.thy
--- a/ESOP-Paper/Paper.thy	Mon Jun 20 20:08:16 2011 +0900
+++ b/ESOP-Paper/Paper.thy	Tue Jun 21 10:37:43 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