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

riscv crefine: set up CBaseRefine 

Signed-off-by: Gerwin Klein <gerwin.klein@data61.csiro.au>
This commit is contained in:
Gerwin Klein 2019-10-14 11:31:51 +11:00 committed by Rafal Kolanski
parent c4f6572aff
commit d0dade06f4
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/RISCV64/Include_C.thy Normal file
View File

@ -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