Jordan/make.ml

   1 (* ========================================================================= *)
   2 (*                          The Jordan Curve Theorem                         *)
   3 (*                                                                           *)
   4 (*                             Proof by Tom Hales                            *)
   5 (*                                                                           *)
   6 (*           A few tweaks by John Harrison for the latest HOL Light          *)
   7 (* ========================================================================= *)
   8
   9 (*** Standard HOL Light library ***)
  10
  11 loads "Library/analysis.ml";;
  12 loads "Library/transc.ml";;
  13 loads "Examples/polylog.ml";;
  14
  15 (*** New stuff ***)
  16
  17 loadt "Jordan/tactics_refine.ml";;
  18 loadt "Jordan/lib_ext.ml";;
  19 loadt "Jordan/tactics_fix.ml";;
  20 loadt "Jordan/parse_ext_override_interface.ml";;
  21 loadt "Jordan/tactics_ext.ml";;
  22 loadt "Jordan/num_ext_gcd.ml";;
  23 loadt "Jordan/num_ext_nabs.ml";;
  24 loadt "Jordan/real_ext_geom_series.ml";;
  25 loadt "Rqe/num_calc_simp.ml";;
  26 loadt "Jordan/real_ext.ml";;
  27 loadt "Jordan/float.ml";;
  28 loadt "Jordan/tactics_ext2.ml";;
  29 loadt "Jordan/misc_defs_and_lemmas.ml";;
  30 loadt "Jordan/metric_spaces.ml";;
  31 loadt "Jordan/jordan_curve_theorem.ml";;