mirror of https://github.com/seL4/l4v.git
lib: introduce Basics session
This session currently contains only one theory (CLib), which we want to include both in Lib and later independently in CParser/AutoCorres. Signed-off-by: Gerwin Klein <gerwin.klein@proofcraft.systems>
This commit is contained in:
parent
2c4c22ccdf
commit
cb34fc3c4c
1
ROOTS
1
ROOTS
|
@ -7,6 +7,7 @@ tools
|
|||
camkes
|
||||
sys-init
|
||||
lib
|
||||
lib/Basics
|
||||
lib/Eisbach_Tools
|
||||
lib/ML_Utils
|
||||
lib/Monads
|
||||
|
|
|
@ -0,0 +1,12 @@
|
|||
(*
|
||||
* Copyright 2023, Proofcraft Pty Ltd
|
||||
*
|
||||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
*)
|
||||
|
||||
chapter Lib
|
||||
|
||||
session Basics (lib) = Word_Lib +
|
||||
|
||||
theories
|
||||
CLib
|
|
@ -20,7 +20,7 @@ imports
|
|||
Eval_Bool
|
||||
Monads.Fun_Pred_Syntax
|
||||
Monads.Monad_Lib
|
||||
CLib
|
||||
Basics.CLib
|
||||
NICTATools
|
||||
"Word_Lib.WordSetup"
|
||||
begin
|
||||
|
|
1
lib/ROOT
1
lib/ROOT
|
@ -9,6 +9,7 @@ chapter Lib
|
|||
session Lib (lib) = Word_Lib +
|
||||
sessions
|
||||
"HOL-Library"
|
||||
Basics
|
||||
Eisbach_Tools
|
||||
ML_Utils
|
||||
Monads
|
||||
|
|
|
@ -6,7 +6,7 @@
|
|||
|
||||
theory LemmaBucket_C
|
||||
imports
|
||||
Lib.CLib
|
||||
Basics.CLib
|
||||
CParser.TypHeapLib
|
||||
begin
|
||||
|
||||
|
|
Loading…
Reference in New Issue