1 needs "flyspeck_needs.hl";; (* snapshot 1631 *)
3 flyspeck_needs "general/sphere.hl";;
5 flyspeck_needs "general/prove_by_refinement.hl";;
7 flyspeck_needs "trigonometry/trig1.hl";;
8 flyspeck_needs "trigonometry/trig2.hl";;
14 open Prove_by_refinement;;
17 #use "euler_complement.ml";;
18 #use "euler_multivariate.ml";;
19 #use "euler_main_theorem.ml";;