needs "tacticlib.ml";; (** some general Tactics; developed to facilitate the process of formalization **)  
needs "cvectors.ml";;  (** Complex Vector Analysis **)
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. **) 
needs "frequency_equalities.ml";; (** Proving that (!x. A*e^(iax)+B*e^(ibx)=C*e^(icx)) ==> a=b=c /\ A+B=C **)
needs "em_model.ml";; (** Formalizaing electromagnetic models, e.g., EM fields, plane waves, interfaces. **)
needs "primitive_rules.ml";; (** Formalizing primitive rules of Optics, e.g., Snell's law and Fresnel Equations **)