1 let flyspeck_dir = "/mnt/Repository/text_formalization";;
\r
2 let hollight_dir = "";;
\r
4 load_path := flyspeck_dir :: !load_path;;
\r
6 let flyspeck_needs = needs;;
\r
9 "Multivariate/flyspeck.ml";
\r
10 "Rqe/num_calc_simp.ml";
\r
11 "general/sphere.hl";
\r
12 "general/prove_by_refinement.hl";
\r
16 let process_to_string unixstring =
\r
17 let p = Unix.open_process_in unixstring
\r
18 and b = Buffer.create 64 in
\r
19 let rec read () = Buffer.add_channel b p 1; read () in
\r
20 try read () with End_of_file -> (Unix.close_process_in p; Buffer.contents b);;
\r
23 open Prove_by_refinement;;
\r
26 "general/flyspeck_lib.hl";
\r
27 "leg/collect_geom2.hl";
\r
28 "leg/enclosed_def.hl";
\r
29 "trigonometry/trig2.hl";
\r
33 "jordan/lib_ext.hl";
\r
34 "jordan/refinement.hl";
\r
35 "jordan/parse_ext_override_interface.hl";
\r
36 "jordan/real_ext.hl";
\r
37 "jordan/hash_term.hl";
\r
43 "jordan/tactics_jordan.hl";
\r
44 "jordan/num_ext_nabs.hl";
\r
45 "jordan/taylor_atn.hl";
\r
47 "jordan/flyspeck_constants.hl";
\r
51 "nonlinear/ineq.hl";
\r
52 "nonlinear/lemma.hl";
\r