From b8e91541f0063b0ca7aa193f5235ba436d65e2c7 Mon Sep 17 00:00:00 2001
From: Matthew Brecknell <Matthew.Brecknell@nicta.com.au>
Date: Tue, 26 Apr 2016 09:27:18 +1000
Subject: [PATCH] arch_split: Bisim checking

---
 proof/bisim/Syscall_S.thy | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/proof/bisim/Syscall_S.thy b/proof/bisim/Syscall_S.thy
index 8eeb910cf..1a88f0a94 100644
--- a/proof/bisim/Syscall_S.thy
+++ b/proof/bisim/Syscall_S.thy
@@ -12,6 +12,8 @@ theory Syscall_S
 imports Separation
 begin
 
+context begin interpretation ARM . (*FIXME: arch_split*)
+
 lemma syscall_bisim:
   assumes bs:
     "bisim (fr \<oplus> r_flt_rel) P P' m_flt m_flt'" 
@@ -819,3 +821,5 @@ lemma call_kernel_separate_state:
   done
 
 end
+
+end