--- a/prio/Paper/document/root.tex	Mon Feb 06 12:08:35 2012 +0000
+++ b/prio/Paper/document/root.tex	Tue Feb 07 00:50:23 2012 +0000
@@ -3,6 +3,7 @@
 \usepackage{isabellesym}
 \usepackage{amsmath}
 \usepackage{amssymb}
+\usepackage{mathpartir}
 %\usepackage{tikz}
 %\usepackage{pgf}
 %\usetikzlibrary{arrows,automata,decorations,fit,calc}
@@ -44,9 +45,9 @@
 \maketitle
 
 \begin{abstract}
-In real-time systems with support for resource locking and for
-processes with priorities, one faces the problem of Priority
-IBnversion. This problem can make the behaviour of processes
+In real-time systems with threads, resource locking and 
+priority sched\-uling, one faces the problem of Priority
+Inversion. This problem can make the behaviour of threads
 unpredictable and the resulting bugs can be hard to find.  The
 Priority Inheritance Protocol is one solution implemented in many
 systems for solving this problem, but the correctness of this solution
@@ -62,7 +63,7 @@
 Paulson's inductive approach to verifying protocols.\medskip
 
 {\bf Keywords:} Priority Inheritance Protocol, formal connectness proof, 
-real-time systems
+real-time systems, Isabelle/HOL
 \end{abstract}
 
 \input{session}