CamkesCdlRefine: add support library for capDL refinement toolchain

This adds a library theory of useful lemmas, simpsets and methods, to be used in the camkes-tool's capDL refinement templates.
seL4 · Jul 15, 2019 · e1ca4ba · e1ca4ba
1 parent fa0b623
commit e1ca4ba
Show file tree

Hide file tree

Showing 2 changed files with 590 additions and 0 deletions.
diff --git a/camkes/ROOT b/camkes/ROOT
@@ -51,6 +51,7 @@ session CamkesCdlRefine (Camkes) in "cdl-refine" = CamkesCdlBase +
   theories
     Generator_CAMKES_CDL
     Policy_CAMKES_CDL
+    Eval_CAMKES_CDL
 
 session CamkesGlueSpec (Camkes) in "glue-spec" = HOL +
   options [document = pdf]