# HG changeset patch
# User chunhan
# Date 1371132932 -28800
# Node ID 64b14b35454e407b241ccc473986a623e5ab3d14
# Parent  4294abb1f38c9755f9cf7269dd180e3be794121f# Parent  8a6e12a9800dc76bf886a08ed31d09d617af1ebc
merge

diff -r 4294abb1f38c -r 64b14b35454e document/christian.jpg
Binary file document/christian.jpg has changed
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
diff -r 4294abb1f38c -r 64b14b35454e document/xingyuan.jpg
Binary file document/xingyuan.jpg has changed