--- a/Paper.thy	Sat Dec 14 13:07:41 2013 +1100
+++ b/Paper.thy	Thu Dec 25 15:54:08 2014 +0000
@@ -52,7 +52,7 @@
 
 
 notation (Rule output)
-  "==>"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
+  "Pure.imp"  ("\<^raw:\mbox{}\inferrule{\mbox{>_\<^raw:}}>\<^raw:{\mbox{>_\<^raw:}}>")
 
 syntax (Rule output)
   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
@@ -67,7 +67,7 @@
   "Trueprop"  ("\<^raw:\mbox{}\inferrule{\mbox{}}{\mbox{>_\<^raw:}}>")
 
 notation (IfThen output)
-  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+  "Pure.imp"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
 syntax (IfThen output)
   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
@@ -75,7 +75,7 @@
   "_asm" :: "prop \<Rightarrow> asms" ("\<^raw:\mbox{>_\<^raw:}>")
 
 notation (IfThenNoBox output)
-  "==>"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
+  "Pure.imp"  ("\<^raw:{\normalsize{}>If\<^raw:\,}> _/ \<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
 syntax (IfThenNoBox output)
   "_bigimpl" :: "asms \<Rightarrow> prop \<Rightarrow> prop"
   ("\<^raw:{\normalsize{}>If\<^raw:\,}> _ /\<^raw:{\normalsize \,>then\<^raw:\,}>/ _.")
@@ -316,7 +316,7 @@
   executing a file, setting a role and setting an UID as well as GID.
   These rules are parametrerised by an arbitrary but fixed access policy.
   Although, there are only four rules, their state-space is in general
-  infinite, like in our work. They therfore give an abstracted semantics,
+  infinite, like in our work. They therefore give an abstracted semantics,
   which gives them a finite state-space. For example the abstracted 
   semantics dispenses with users and roles by introducing
   abstract users and abstract roles. They obtain a soundness result