Update from HH
[hl193./.git] / 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";;