===============================================================================
               Formal development of the paper
      ``On the Formal Analysis of Optical Systems''
===============================================================================


DESCRIPTION:

  See each file individually for a description of their contents in their
  header.


INSTALLATION:

  Tested with the latest svn version of HOL Light (July 2014).

  How to use:

  1. Go to the HOL Light directory

  2. Launch ocaml

  3. Type in:

    > #use "hol.ml";;
    
  4. Once everything has loaded, type in:

    > List.iter needs ["Multivariate/make_complex.ml";"Multivariate/geom.ml";
  "Multivariate/cross.ml";"Multivariate/wlog.ml"];;

    (this takes a while, but not more than 1hrs on our machines)

  6. Then move (in ocaml) to the directory containing our files:

    > #cd "path/to/directory";;

  7. And finally load the top file:

    > needs "top.ml";;
    
    (this will also load all the intermediate files)