Rqe/make.ml

   1 (* ------------------------------------------------------------------------- *)
   2 (* Library requirements.                                                     *)
   3 (* ------------------------------------------------------------------------- *)
   4
   5 needs "Library/analysis.ml";;
   6 needs "Library/poly.ml";;
   7
   8 (* ------------------------------------------------------------------------- *)
   9 (* The main code.                                                            *)
  10 (* ------------------------------------------------------------------------- *)
  11
  12 loads "Rqe/rqe_lib.ml";;
  13 loads "Rqe/rqe_tactics_ext.ml";;
  14 loads "Rqe/util.ml";;
  15 loads "Rqe/rewrites.ml";;
  16 loads "Rqe/basic.ml";;
  17 loads "Rqe/rqe_num.ml";;
  18 loads "Rqe/rqe_real.ml";;
  19 loads "Rqe/list_rewrites.ml";;
  20 loads "Rqe/rqe_list.ml";;
  21 loads "Rqe/timers.ml";;
  22 loads "Rqe/num_calc_simp.ml";;
  23 loads "Rqe/asym.ml";;
  24 loads "Rqe/rol.ml";;
  25 loads "Rqe/poly_ext.ml";;
  26 loads "Rqe/simplify.ml";;
  27 loads "Rqe/lift_qelim.ml";;
  28 loads "Rqe/defs.ml";;
  29 loads "Rqe/testform_thms.ml";;
  30 loads "Rqe/condense_thms.ml";;
  31 loads "Rqe/inferisign_thms.ml";;
  32 loads "Rqe/matinsert_thms.ml";;
  33 loads "Rqe/signs_thms.ml";;
  34 loads "Rqe/inferpsign_thms.ml";;
  35 loads "Rqe/dedmatrix_thms.ml";;
  36 loads "Rqe/pdivides_thms.ml";;
  37 loads "Rqe/main_thms.ml";;
  38 loads "Rqe/work_thms.ml";;
  39 loads "Rqe/testform.ml";;
  40 loads "Rqe/condense.ml";;
  41 loads "Rqe/inferisign.ml";;
  42 loads "Rqe/matinsert.ml";;
  43 loads "Rqe/signs.ml";;
  44 loads "Rqe/inferpsign.ml";;
  45 loads "Rqe/dedmatrix.ml";;
  46 loads "Rqe/pdivides.ml";;
  47 loads "Rqe/rqe_main.ml";;
  48
  49 (****
  50 loads "Rqe/examples.ml";;
  51  ****)