# HG changeset patch
# User Christian Urban <christian dot urban at kcl dot ac dot uk>
# Date 1419522848 0
# Node ID 17ea9ad46257f48edf84af6e74fdb32f361e3f88
# Parent  928c015eb03eb31bb20c5012b387af26a57e9853
updated for Isabelle 2014

diff -r 928c015eb03e -r 17ea9ad46257 Paper.thy
--- 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
diff -r 928c015eb03e -r 17ea9ad46257 del_vs_del_s.thy
--- a/del_vs_del_s.thy	Sat Dec 14 13:07:41 2013 +1100
+++ b/del_vs_del_s.thy	Thu Dec 25 15:54:08 2014 +0000
@@ -139,7 +139,7 @@
   with exp initp vs' obtain r fr pt u 
     where SP: "obj2sobj s' (Proc p) = SProc (r,fr,pt,u) (Some p)"
     apply (frule_tac current_proc_has_sobj, simp)
-    by (simp add:obj2sobj.simps split:option.splits, blast)
+    by (simp add:obj2sobj.simps split:option.splits)
   with exp vs' all_sobjs_I[where s = s' and obj = "Proc p"]
   have SP_in: "SProc (r,fr,pt,u) (Some p) \<in> all_sobjs" by simp
 
diff -r 928c015eb03e -r 17ea9ad46257 document/isabelle.sty
--- a/document/isabelle.sty	Sat Dec 14 13:07:41 2013 +1100
+++ b/document/isabelle.sty	Thu Dec 25 15:54:08 2014 +0000
@@ -97,6 +97,8 @@
 \chardef\isachartilde=`\~%
 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
+\def\isacartoucheopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
+\def\isacartoucheclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
 }
 
 
@@ -195,6 +197,12 @@
 \chardef\isacharbackquoteclose=`\`%
 }
 
+\newcommand{\isabellestyleliteralunderscore}{%
+\isabellestyleliteral%
+\def\isacharunderscore{\textunderscore}%
+\def\isacharunderscorekeyword{\textunderscore}%
+}
+
 \newcommand{\isabellestylesl}{%
 \isabellestyleit%
 \def\isastyle{\small\sl}%
diff -r 928c015eb03e -r 17ea9ad46257 document/isabellesym.sty
--- a/document/isabellesym.sty	Sat Dec 14 13:07:41 2013 +1100
+++ b/document/isabellesym.sty	Thu Dec 25 15:54:08 2014 +0000
@@ -354,3 +354,7 @@
 \newcommand{\isasymbind}{\isamath{\mathbin{>\!\!\!>\mkern-6.7mu=}}}
 \newcommand{\isasymthen}{\isamath{\mathbin{>\!\!\!>}}}
 \newcommand{\isasymsome}{\isamath{\epsilon\,}}
+\newcommand{\isasymopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}
+\newcommand{\isasymclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}
+\newcommand{\isasymnewline}{\isatext{\fbox{$\hookleftarrow$}}}
+
diff -r 928c015eb03e -r 17ea9ad46257 os_rc.thy
--- a/os_rc.thy	Sat Dec 14 13:07:41 2013 +1100
+++ b/os_rc.thy	Thu Dec 25 15:54:08 2014 +0000
@@ -352,7 +352,7 @@
 apply (simp add:fname_length_set_def) 
 apply (rule finite_imageI) using finite_cf[where s = s]
 apply (drule_tac h = "\<lambda> f'. case f' of [] \<Rightarrow> '''' | fn # pf' \<Rightarrow> if (pf' = f) then fn else ''''" in finite_imageI)
-apply (rule_tac B = "(list_case [] (\<lambda>fn pf'. if pf' = f then fn else []) ` current_files s)" in finite_subset)
+apply (rule_tac B = "(case_list [] (\<lambda>fn pf'. if pf' = f then fn else []) ` current_files s)" in finite_subset)
 unfolding image_def
 apply(auto)[1]
 apply (rule_tac x = "x # f" in bexI, simp+)
diff -r 928c015eb03e -r 17ea9ad46257 slides1.pdf
Binary file slides1.pdf has changed