Journal/Paper.thy
changeset 24 6f50e6a8c6e0
parent 23 24e6884d9258
child 25 a9c0eeb00cc3
--- 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