Update from HH
[Flyspeck/.git] / legacy / oldtrig / run_file_euler.ml
1 needs "flyspeck_needs.hl";;   (* snapshot 1631 *)
2
3 flyspeck_needs "general/sphere.hl";;
4
5 flyspeck_needs "general/prove_by_refinement.hl";;
6
7 flyspeck_needs "trigonometry/trig1.hl";;
8 flyspeck_needs "trigonometry/trig2.hl";;
9
10
11 open Sphere;;
12 open Trigonometry1;;
13 open Trigonometry2;;
14 open Prove_by_refinement;;
15
16 #use "delta_x.ml";;
17 #use "euler_complement.ml";;
18 #use "euler_multivariate.ml";;
19 #use "euler_main_theorem.ml";;
20
21
22