(* ========================================================================= *)
(*                                                                           *)
(*                        Formal Analysis of Geometrical Optics              *)
(*                                                                           *)
(*        (c) Copyright, Umair Siddique, 2012-2015                           *)
(*                       Hardware Verification Group,                        *)
(*                       Concordia University                                *)
(*                                                                           *)
(*     Contact: <muh_sidd@ece.concordia.ca>                                  *)
(*                                                                           *)
(* Last update: Sep  2015                                                    *)
(*                                                                           *)
(* ========================================================================= *)

DESCRIPTION:

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


INSTALLATION:

  Tested with the latest svn version of HOL Light 
  

  How to use:

  1. Go to the HOL Light directory

  2. Launch ocaml

  3. Type in:

    > #use "hol.ml";;
      

  4. Unzip sources.zip and move (in ocaml) to the directory (sources_goptics) containing three directories:
     e.g., cardinal_points, gaussian or resonator

    > #cd "path/to/directory";;
    e.g., #cd "path/to/resonator";;

  5. And finally load the top file:

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