# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1393926040 0
# Node ID 6f50e6a8c6e06f27dc9d5c126951c89c8cdc91a5
# Parent  24e6884d9258b2d679414f15af164f5388454579
some additions

diff -r 24e6884d9258 -r 6f50e6a8c6e0 Journal/Paper.thy
--- a/Journal/Paper.thy	Tue Mar 04 08:45:11 2014 +0000
+++ b/Journal/Paper.thy	Tue Mar 04 09:40:40 2014 +0000
@@ -28,7 +28,7 @@
   original_priority ("priority") and
   DUMMY  ("\<^raw:\mbox{$\_\!\_$}>")
 
-
+ 
 (*>*)
 
 section {* Introduction *}
@@ -1465,7 +1465,7 @@
   pointed out an error in a paper about Preemption 
   Threshold Scheduling \cite{ThreadX}. The use of a theorem prover was
   invaluable to us in order to be confident about the correctness of our reasoning 
-  (no case can be overlooked).  
+  (no case can be overlooked).   
   The most closely related work to ours is the formal verification in
   PVS of the Priority Ceiling Protocol done by Dutertre
   \cite{dutertre99b}---another solution to the Priority Inversion
diff -r 24e6884d9258 -r 6f50e6a8c6e0 Journal/document/root.bib
--- a/Journal/document/root.bib	Tue Mar 04 08:45:11 2014 +0000
+++ b/Journal/document/root.bib	Tue Mar 04 09:40:40 2014 +0000
@@ -73,7 +73,7 @@
 @inproceedings{ZhangUrbanWu12,
   author    = {X.~Zhang and C.~Urban and C.~Wu},
   title     = {{P}riority {I}nheritance {P}rotocol {P}roved {C}orrect},
-  booktitle = {Proc.~of the 3rd Conference on Interactive Theorem Proving},
+  booktitle = {Proc.~of the 3rd Conference on Interactive Theorem Proving (ITP)},
   year      = {2012},
   pages     = {217--232},
   series    = {LNCS},
diff -r 24e6884d9258 -r 6f50e6a8c6e0 Journal/document/root.tex
--- a/Journal/document/root.tex	Tue Mar 04 08:45:11 2014 +0000
+++ b/Journal/document/root.tex	Tue Mar 04 09:40:40 2014 +0000
@@ -48,7 +48,7 @@
 
 \begin{document}
 \renewcommand{\thefootnote}{$\star$}
-\footnotetext[1]{This is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}.}
+\footnotetext[1]{This paper is a revised, corrected and expanded version of \cite{ZhangUrbanWu12}.}
 \renewcommand{\thefootnote}{\arabic{footnote}}
 
 \title{Priority Inheritance Protocol Proved Correct}
diff -r 24e6884d9258 -r 6f50e6a8c6e0 journal.pdf
Binary file journal.pdf has changed