top.ml

   1
   2 needs "tacticlib.ml";; (** some general Tactics; developed to facilitate the process of formalization **)
   3 needs "cvectors.ml";;  (** Complex Vector Analysis **)\r
   4 needs "vectors_ext.ml";;  (** some notion in real vector analysis we need in developing EM Optics, e.g., unit vector and projection on hyper plains. **) \r
   5 needs "frequency_equalities.ml";; (** Proving that (!x. A*e^(iax)+B*e^(ibx)=C*e^(icx)) ==> a=b=c /\ A+B=C **)
   6 needs "em_model.ml";; (** Formalizaing electromagnetic models, e.g., EM fields, plane waves, interfaces. **)
   7 needs "primitive_rules.ml";; (** Formalizing primitive rules of Optics, e.g., Snell's law and Fresnel Equations **)
   8 \r
   9
  10 \r
  11