The source files should be built with Abella v2.0.5.
The proof scripts are organized in a linearly dependent style, i.e. each file depend on its previous one following the list:
- olist.thm
- nat.thm
- higher.thm
- order.thm
- higher_alg.thm
- trans.thm
- sound.thm
- depth.thm
- complete.thm
- decidable.thm