adbrucker
/
lh-l4v
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

x64: crefine: add Include_C

This commit is contained in:
Joel Beeren 2017-08-15 14:49:41 +10:00
parent 85a20c08a5
commit 92f5d14c0b
1 changed files with 17 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

17
proof/crefine/X64/Include_C.thy Normal file
View File

@ -0,0 +1,17 @@
(*
* Copyright 2017, 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
"../../../spec/cspec/$L4V_ARCH/KernelInc_C"
"../../refine/$L4V_ARCH/Refine"
begin
end