| (* |
| * 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" |
