1 (* ========================================================================= *)
2 (* The Jordan Curve Theorem *)
4 (* Proof by Tom Hales *)
6 (* A few tweaks by John Harrison for the latest HOL Light *)
7 (* ========================================================================= *)
9 (*** Standard HOL Light library ***)
14 needs "Rqe/num_calc_simp.ml";;
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";;
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";;