--- a/Journal/document/root.tex	Mon Jan 15 11:35:56 2018 +0000
+++ b/Journal/document/root.tex	Tue Feb 06 14:38:31 2018 +0000
@@ -83,7 +83,7 @@
   solution proposed earlier. We also generalise the scheduling problem
   to the practically relevant case where critical sections can
   overlap. Our formalisation in Isabelle/HOL is based on Paulson's
-  inductive approach to verifying protocols.  The formalisation not
+  inductive approach to  protocol verification.  The formalisation not
   only uncovers facts overlooked in the literature, but also helps
   with an efficient implementation of this protocol. Earlier
   implementations were criticised as too inefficient. Our