The theory files can be checked with Isabelle 2013-2. Isabelle 2013-1 and other older verisions are not compatible.
- all.thy: theory which imports all other theory-files ( can be used to find unused theorems in all files and to load everything at once)
- src/framework: Contains the general framework which applies to all CRDTs
- src/crdts: Contains the different verified CRDTs. For each CRDT there are several files with the following postfixes:
- ..._spec: the specification of the data type
- ..._[implementation-name]: an implementation of the data type
- ..._[implementation-name]_convergence: convergence proofs for the implementation
- ..._[implementation-name]_valid: proofs that the implementation is conform to specification