--- 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