X-Git-Url: https://git.stderr.nl/gitweb?p=matthijs%2Fmaster-project%2Freport.git;a=blobdiff_plain;f=Chapters%2FNormalization.tex;h=8058a1596c8683fb7da8ea5af9501ca78d555a3d;hp=5252c0fe71bca473d5ff2deb71482a7bbeed2d2a;hb=51c4ee734de45dac80f73cab386164e1e8e4098e;hpb=23487a1fa3e35868cd9d838eb3c59d02ed5ebdac

diff --git a/Chapters/Normalization.tex b/Chapters/Normalization.tex
index 5252c0f..8058a15 100644
--- a/Chapters/Normalization.tex
+++ b/Chapters/Normalization.tex
@@ -2568,9 +2568,8 @@
       {\lam{\forall A, B, C \exists D (A ->> B ∧ A ->> C => B ->> D ∧ C ->> D)}}
 
     Here, \lam{A ->> B} means \lam{A} \emph{reduces to} \lam{B}. In
-    other words, there is a set of transformations that can be applied
-    to transform \lam{A} to \lam{B}. \lam{=>} is used to mean
-    \emph{implies}.
+    other words, there is a set of transformations that can transform
+    \lam{A} to \lam{B}. \lam{=>} is used to mean \emph{implies}.
 
     For a transformation system holding the Church-Rosser property, it
     is easy to show that it is in fact deterministic. Showing that this