From d0dade06f41c311f29af527cb44d549217e3a79b Mon Sep 17 00:00:00 2001
From: Gerwin Klein <gerwin.klein@data61.csiro.au>
Date: Mon, 14 Oct 2019 11:31:51 +1100
Subject: [PATCH] riscv crefine: set up CBaseRefine

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
---
 proof/crefine/RISCV64/Include_C.thy | 17 +++++++++++++++++
 1 file changed, 17 insertions(+)
 create mode 100644 proof/crefine/RISCV64/Include_C.thy

diff --git a/proof/crefine/RISCV64/Include_C.thy b/proof/crefine/RISCV64/Include_C.thy
new file mode 100644
index 000000000..40d501336
--- /dev/null
+++ b/proof/crefine/RISCV64/Include_C.thy
@@ -0,0 +1,17 @@
+(*
+ * Copyright 2019, Data61, CSIRO
+ *
+ * This software may be distributed and modified according to the terms of
+ * the GNU General Public License version 2. Note that NO WARRANTY is provided.
+ * See "LICENSE_GPLv2.txt" for details.
+ *
+ * @TAG(DATA61_GPL)
+ *)
+
+theory Include_C
+imports
+  "CSpec.KernelInc_C"
+  "Refine.Refine"
+begin
+
+end