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

x64: add crefine stubs to keep theory_imports happy

This commit is contained in:
Matthew Brecknell 2017-07-31 13:30:25 +10:00
parent b5bb4e083c
commit 3871575834
2 changed files with 36 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

19
proof/crefine/X64/Refine_C.thy Normal file
View File

@ -0,0 +1,19 @@
(*
* 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)
*)
chapter "Toplevel Refinement Statement"
(* Stub to keep the theory_imports check happy
until we're ready to write some proofs here. *)
theory Refine_C
imports Main
begin
end

17
proof/crefine/X64/SR_lemmas_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)
*)
(* Stub to keep the theory_imports check happy
until we're ready to write some proofs here. *)
theory SR_lemmas_C
imports Main
begin
end