# HG changeset patch
# User urbanc
# Date 1331033445 0
# Node ID f9d54f49c808ba85136b1e77f42d7d4c68ed235a
# Parent  f9e0d3274c14473fdba2c3a6126aeca592a7e310
typo

diff -r f9e0d3274c14 -r f9d54f49c808 prio/Paper/Paper.thy
--- 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
diff -r f9e0d3274c14 -r f9d54f49c808 prio/paper.pdf
Binary file prio/paper.pdf has changed