----------------------------------------------------------------------
===============================================================================
               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 (December 2013).

  How to use:

  1. Go to the HOL Light directory

  2. Launch ocaml

  3. Type in:

    > #use "hol.ml";;
      

  4. Unzip ray.zip and move (in ocaml) to the directory containing our files:

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

  5. And finally load the top file:

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