let flyspeck_dir = "/mnt/Repository/text_formalization";; let hollight_dir = "";; load_path := flyspeck_dir :: !load_path;; let flyspeck_needs = needs;; map needs [ "Multivariate/flyspeck.ml"; "Rqe/num_calc_simp.ml"; "general/sphere.hl"; "general/prove_by_refinement.hl"; ];; #load "unix.cma";; let process_to_string unixstring = let p = Unix.open_process_in unixstring and b = Buffer.create 64 in let rec read () = Buffer.add_channel b p 1; read () in try read () with End_of_file -> (Unix.close_process_in p; Buffer.contents b);; open Prove_by_refinement;; map needs [ "general/flyspeck_lib.hl"; "leg/collect_geom2.hl"; "leg/enclosed_def.hl"; "trigonometry/trig2.hl"; ];; map needs [ "jordan/lib_ext.hl"; "jordan/refinement.hl"; "jordan/parse_ext_override_interface.hl"; "jordan/real_ext.hl"; "jordan/hash_term.hl"; ];; prioritize_real();; map needs [ "jordan/tactics_jordan.hl"; "jordan/num_ext_nabs.hl"; "jordan/taylor_atn.hl"; "jordan/float.hl"; "jordan/flyspeck_constants.hl"; ];; map needs [ "nonlinear/ineq.hl"; "nonlinear/lemma.hl"; ];;