--- a/prio/Paper/Paper.thy	Tue Feb 28 13:13:32 2012 +0000
+++ b/prio/Paper/Paper.thy	Tue Mar 06 11:30:45 2012 +0000
@@ -644,7 +644,7 @@
   that in every future state (denoted by @{text "s' @ s"}) in which
   @{text th} is still alive, either @{text th} is running or it is
   blocked by a thread that was alive in the state @{text s} and was waiting 
-  or in the possession of a lock in @{text s}. Since in @{text s}, as in
+  for or in the possession of a lock in @{text s}. Since in @{text s}, as in
   every state, the set of alive threads is finite, @{text th} can only
   be blocked a finite number of times. This is independent of how many
   threads of lower priority are created in @{text "s'"}. We will actually prove a