| (* | |
| * Copyright 2016, NICTA | |
| * | |
| * This software may be distributed and modified according to the terms of | |
| * the BSD 2-Clause license. Note that NO WARRANTY is provided. | |
| * See "LICENSE_BSD2.txt" for details. | |
| * | |
| * @TAG(NICTA_BSD) | |
| *) | |
| session CogentCRefinement = CogentShallow + | |
| theories | |
| Cogent_C_Heap_Auto | |
| Cogent_Corres | |
| Cogent_Corres_Sanity_Check | |
| Cogent_Corres_Shallow_C | |
| Cogent_C_Val_Auto | |
| CogentHigherOrder | |
| Corres_Tac | |
| Deep_Embedding_Auto | |
| Heap_Relation_Generation | |
| Read_Table | |
| Specialised_Lemma | |
| SpecialisedLemmaTactic | |
| Specialised_Lemma_URecord | |
| Specialised_Lemma_USum | |
| Specialised_Lemma_Utils | |
| Tidy | |
| Type_Args | |
| Type_Relation_Generation | |
| Utils | |
| Value_Relation | |
| Value_Relation_Generation |