(*
 * Copyright 2016, NICTA
 *
 * 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(NICTA_GPL)
 *)

(*
session CogentUtil = "Word_Lib" +
  sessions "Eisbach"
  theories "Cogent.Util"
*)

session "BilbyFsCode" (main) = CogentCRefinement +
  description {* BilbyFs implementation *}
  theories
  "impl/BilbyFs_Shallow_Desugar_Tuples"

session "BilbyFsConsts" = "BilbyFsCode" +
  description {* BilbyFs consts *}
  theories
  "impl/BilbyFs_ShallowConsts_Desugar_Tuples"

session BilbyFs = "BilbyFsConsts" +
  theories "lib/L4vBucket"

session BilbyFsSync = "BilbyFs" +
  theories
   "refine/FsopSyncR"

session BilbyFsIget = "BilbyFs" +
  theories
   "refine/FsopIgetR"