needs "Library/analysis.ml";; (* Basic real analysis *) needs "Library/transc.ml";; (* Real transcendental functions *) needs "Library/floor.ml";; (* Floor and frac functions *) needs "Complex/complexnumbers.ml";; (* Basic complex number defs *) needs "Complex/complex_transc.ml";; (* Complex transcendental functions *) needs "Complex/cpoly.ml";; (* Complex polynomials *) needs "Complex/fundamental.ml";; (* Fundamental theorem of algebra *) needs "Complex/quelim.ml";; (* Quantifier elimination algorithm *) needs "Complex/complex_grobner.ml";; (* Grobner bases with HOL proofs *) needs "Complex/complex_real.ml";; (* Special case of reals *) needs "Complex/quelim_examples.ml";; (* Examples of using quantifier elim *) needs "Complex/grobner_examples.ml";; (* Examples of using Grobner bases *)