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