Objective Caml code supporting John Harrison's logic textbook Handbook of Practical Logic and Automated Reasoning.
The original code work with OCaml 3.x.
This repo contains sligth modifications and instructions to fit OCaml 4.
The Num library (for arbitrary-precision integer and rational arithmetic) is no longer part of the core OCaml distribution since OCaml version 4.06.0
You need to : opam install num
make compiled generate an executable binary named example