text_formalization/jordan/make.hl

   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
  12 (*** New stuff ***)
  13
  14 needs "Rqe/num_calc_simp.ml";;
  15
  16 flyspeck_needs "jordan/tactics_refine.ml";;
  17 flyspeck_needs "jordan/lib_ext.ml";;
  18 flyspeck_needs "jordan/tactics_fix.ml";;
  19 flyspeck_needs "jordan/parse_ext_override_interface.ml";;
  20 flyspeck_needs "jordan/tactics_ext.ml";;
  21 flyspeck_needs "jordan/num_ext_gcd.ml";;
  22 flyspeck_needs "jordan/num_ext_nabs.ml";;
  23 flyspeck_needs "jordan/real_ext_geom_series.ml";;
  24 flyspeck_needs "jordan/real_ext.ml";;
  25 flyspeck_needs "jordan/float.ml";;
  26 flyspeck_needs "jordan/tactics_ext2.ml";;
  27 flyspeck_needs "jordan/misc_defs_and_lemmas.ml";;
  28
  29 (*  (* need to be reworked.  These don't currently load *)
  30 flyspeck_needs "Jordan/compute_pi.ml";;
  31 flyspeck_needs "Jordan/metric_spaces.ml";;
  32 flyspeck_needs "Jordan/jordan_curve_theorem.ml";;
  33 *)