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 **)