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

x64: change Refine_C to point to TcbQueue_C for regression testing

This commit is contained in:
Joel Beeren 2017-09-13 17:13:12 +10:00
parent ae707eb153
commit 7c54fc69dd
1 changed files with 2 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

5
proof/crefine/X64/Refine_C.thy
View File

@ -10,10 +10,9 @@
chapter "Toplevel Refinement Statement"
(* Stub to keep the theory_imports check happy
until we're ready to write some proofs here. *)
(* In progress c refinement *)
theory Refine_C
imports Main
imports TcbQueue_C
begin
end