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