This directory contains the script that does in-logic compilation of the OpenTheory article checker.
ag32: Compilation of the OpenTheory article checker to the Silver ISA.
proofs: The directory contains end-to-end correctness theorems for the OpenTheory article checker.
readerCompileScript.sml: Compiles the OpenTheory article checker in the logic.