diff --git a/proof/ROOT b/proof/ROOT
index 4ed00b7a0..2ea7c46c0 100644
--- a/proof/ROOT
+++ b/proof/ROOT
@@ -206,6 +206,8 @@ session SimplExportAndRefine in "asmrefine" = SimplExport +
     "SEL4GraphRefine"
 
 session SimplExport in "asmrefine/export" = CSpec +
+  directories
+    "$L4V_ARCH"
   theories
     "SEL4SimplExport"
 
diff --git a/proof/asmrefine/export/ARM/ArchSEL4SimplExport.thy b/proof/asmrefine/export/ARM/ArchSEL4SimplExport.thy
new file mode 100644
index 000000000..1f9849c7d
--- /dev/null
+++ b/proof/asmrefine/export/ARM/ArchSEL4SimplExport.thy
@@ -0,0 +1,31 @@
+(*
+ * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+ *
+ * SPDX-License-Identifier: GPL-2.0-only
+ *)
+
+theory ArchSEL4SimplExport
+imports "AsmRefine.SimplExport" "CSpec.Substitute"
+begin
+
+context kernel_all_substitute begin
+
+lemma ctzl_body_refines:
+  "simple_simpl_refines \<Gamma> (Guard ImpossibleSpec \<lbrace>\<acute>x \<noteq> 0\<rbrace>
+    (\<acute>ret__long :== ucast (bv_ctz (\<acute>x)))) ctzl_body"
+  apply (simp add: ctzl_body_def)
+  apply (rule simple_simpl_refines_guarded_Basic_guarded_spec_body)
+  apply (clarsimp simp: bv_ctz_def meq_def)
+  done
+
+lemma clzl_body_refines:
+  "simple_simpl_refines \<Gamma> (Guard ImpossibleSpec \<lbrace>\<acute>x \<noteq> 0\<rbrace>
+    (\<acute>ret__long :== ucast (bv_clz (\<acute>x)))) clzl_body"
+  apply (simp add: clzl_body_def)
+  apply (rule simple_simpl_refines_guarded_Basic_guarded_spec_body)
+  apply (clarsimp simp: bv_clz_def meq_def)
+  done
+
+end
+
+end
diff --git a/proof/asmrefine/export/RISCV64/ArchSEL4SimplExport.thy b/proof/asmrefine/export/RISCV64/ArchSEL4SimplExport.thy
new file mode 100644
index 000000000..eacc27983
--- /dev/null
+++ b/proof/asmrefine/export/RISCV64/ArchSEL4SimplExport.thy
@@ -0,0 +1,11 @@
+(*
+ * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
+ *
+ * SPDX-License-Identifier: GPL-2.0-only
+ *)
+
+theory ArchSEL4SimplExport
+imports "AsmRefine.SimplExport"
+begin
+
+end
diff --git a/proof/asmrefine/export/SEL4SimplExport.thy b/proof/asmrefine/export/SEL4SimplExport.thy
index 7a1c9a26a..0b86eff6b 100644
--- a/proof/asmrefine/export/SEL4SimplExport.thy
+++ b/proof/asmrefine/export/SEL4SimplExport.thy
@@ -5,7 +5,7 @@
  *)
 
 theory SEL4SimplExport
-imports "AsmRefine.SimplExport" "CSpec.Substitute"
+imports "ArchSEL4SimplExport" "CSpec.Substitute"
 begin
 
 ML \<open>
@@ -16,22 +16,6 @@ val csenv = let
 
 context kernel_all_substitute begin
 
-lemma ctzl_body_refines:
-  "simple_simpl_refines \<Gamma> (Guard ImpossibleSpec \<lbrace>\<acute>x \<noteq> 0\<rbrace>
-    (\<acute>ret__long :== ucast (bv_ctz (\<acute>x)))) ctzl_body"
-  apply (simp add: ctzl_body_def)
-  apply (rule simple_simpl_refines_guarded_Basic_guarded_spec_body)
-  apply (clarsimp simp: bv_ctz_def meq_def)
-  done
-
-lemma clzl_body_refines:
-  "simple_simpl_refines \<Gamma> (Guard ImpossibleSpec \<lbrace>\<acute>x \<noteq> 0\<rbrace>
-    (\<acute>ret__long :== ucast (bv_clz (\<acute>x)))) clzl_body"
-  apply (simp add: clzl_body_def)
-  apply (rule simple_simpl_refines_guarded_Basic_guarded_spec_body)
-  apply (clarsimp simp: bv_clz_def meq_def)
-  done
-
 declare ctcb_offset_defs[simp]
 
 ML \<open>
@@ -44,4 +28,3 @@ ML \<open>
 end
 
 end
-