diff -r 4294abb1f38c -r 64b14b35454e document/root.tex
--- a/document/root.tex	Thu Jun 13 22:12:45 2013 +0800
+++ b/document/root.tex	Thu Jun 13 22:15:32 2013 +0800
@@ -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