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 ***)
11 loads "Library/analysis.ml";;
12 loads "Library/transc.ml";;
13 loads "Examples/polylog.ml";;
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";;