# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1371121299 14400
# Node ID 8a6e12a9800dc76bf886a08ed31d09d617af1ebc
# Parent  8b6ba7168f2d4e958ee75b96d94f0b9e85c48876
updated

diff -r 8b6ba7168f2d -r 8a6e12a9800d document/root.tex
--- a/document/root.tex	Tue Apr 30 14:46:18 2013 +0100
+++ b/document/root.tex	Thu Jun 13 07:01:39 2013 -0400
@@ -105,7 +105,7 @@
 of events that will compromise it.  Consequently, a static policy
 check is sufficient (sound and complete) in order to guarantee or
 expose the security of resources before running the system.  Our
-formal models and correctness proofs are mechanised in the
+formal model and correctness proof are mechanised in the
 Isabelle/HOL theorem prover using Paulson's inductive method for
 reasoning about valid sequences of events. Our results apply to the
 Role-Compatibility Model, but can be readily adapted to other