diff -r f87e6e23bf17 -r 21c980a85ee5 thys/Paper/Paper.thy
--- a/thys/Paper/Paper.thy	Tue Mar 08 07:13:20 2016 +0000
+++ b/thys/Paper/Paper.thy	Tue Mar 08 07:14:52 2016 +0000
@@ -947,7 +947,7 @@
   their greedy matching algorithm always produces a maximal element
   according to this ordering (from all possible solutions). The only
   difference between their greedy ordering and the ``ordering'' by Sulzmann
-  and Lu is that GREEDY always prefers a $Left$-value over a $Right-value$.
+  and Lu is that GREEDY always prefers a $Left$-value over a $Right$-value.
   What is interesting for our purposes is that the properties reflexivity,
   totality and transitivity for this GREEDY ordering can be proved
   relatively easily by induction.