# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1315565544 -3600
# Node ID 4df720c9b660707ebba19f54bd145393d654e89f
# Parent  c6af56de923debfc7d497d5a81b06f50604c5438# Parent  8e8aabf01f52bf678dd2c47e9b3c02b1df35531f
merged

diff -r c6af56de923d -r 4df720c9b660 LMCS-Paper/Paper.thy
--- a/LMCS-Paper/Paper.thy	Thu Sep 08 13:03:19 2011 +0100
+++ b/LMCS-Paper/Paper.thy	Fri Sep 09 11:52:24 2011 +0100
@@ -359,7 +359,7 @@
   infrastructure for alpha-equated terms.\smallskip
 
   The examples we have in mind where our reasoning infrastructure will be
-  helpful includes the term language of Core-Haskell (see
+  helpful include the term language of Core-Haskell (see
   Figure~\ref{corehas}). This term language involves patterns that have lists
   of type-, coercion- and term-variables, all of which are bound in @{text
   "\<CASE>"}-expressions. In these patterns we do not know in advance how many
@@ -571,7 +571,7 @@
   
   \begin{equation}\label{equivariance}
   @{text "\<pi> \<bullet> f = f"} \;\;\;\;\textit{if and only if}\;\;\;\;
-  @{text "\<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}
+  @{text "\<forall>x. \<pi> \<bullet> (f x) = f (\<pi> \<bullet> x)"}
   \end{equation}\smallskip
    
   \noindent