# HG changeset patch
# User chunhan
# Date 1370501452 -28800
# Node ID de8733706a0681b01eb8f27c53e1cc3fa398faeb
# Parent  e2c6af3ccb0d6bd920e1b5701fcb1569ce67c169
update

diff -r e2c6af3ccb0d -r de8733706a06 Dynamic2static.thy
--- a/Dynamic2static.thy	Thu Jun 06 12:38:44 2013 +0800
+++ b/Dynamic2static.thy	Thu Jun 06 14:50:52 2013 +0800
@@ -213,12 +213,8 @@
 apply (case_tac obj, simp_all split:option.splits if_splits)
 apply (drule_tac sm = "(aa, ba, True)" in sq_sm_prop, simp+, erule exE)
 apply (rule_tac x = "O_msg nat m" in exI)
-apply (simp)
-
-apply (case_tac obj, (simp split:option.splits if_splits)+)
-apply (erule conjE, drule_tac )
-
-
+apply (simp add:cm2smsg_def split:option.splits)
+done
 
 lemma has_inode_tainted_aux:
   "O_file f \<in> tainted s \<Longrightarrow> \<forall> f'. has_same_inode s f f' \<longrightarrow> O_file f' \<in> tainted s"