MetaPRL OCaml Support

MetaPRL provides built-in support for OCaml with two theory directories: theories/ocaml and theories/ocaml_sos. The first directory contains display definitions for OCaml, and the second contains an operational semantics for OCaml.

This document is not yet complete. There are three main issues to discuss:

1. What is the logical representation of OCaml programs?
2. What is the operational semantics?
3. What is the interpretation in Nuprl type theory?