(* ==== Loaded files from Vu Khac Ky - 22 Mar 2012 ========================= *)

#use "/usr/programs/hollight/hollight-114/hol.ml";; 
loads "Multivariate/flyspeck.ml";;
#use "/home/vu/flyspeck/working/boot.hl";;               (* hol_version 2734 *) 
flyspeck_needs "trigonometry/trig1.hl";;
flyspeck_needs "trigonometry/trig2.hl";;
flyspeck_needs "trigonometry/euler_main_theorem.hl";;
flyspeck_needs "leg/muR_def.hl";;
flyspeck_needs "leg/enclosed_def.hl";;
flyspeck_needs "trigonometry/trigonometry.hl";;
flyspeck_needs "leg/collect_geom.hl";;
flyspeck_needs "fan/fan_defs.hl";;
flyspeck_needs "fan/introduction.hl";; 
flyspeck_needs "fan/topology.hl";;
flyspeck_needs "fan/fan_misc.hl";; 
flyspeck_needs "fan/HypermapAndFan.hl";; 
flyspeck_needs "packing/pack_defs.hl";;
flyspeck_needs "packing/pack_concl.hl";; 
flyspeck_needs "packing/pack1.hl";;
flyspeck_needs "packing/pack2.hl";;
flyspeck_needs "packing/pack3.hl";;
flyspeck_needs "packing/Rogers.hl";; 
flyspeck_needs "nonlinear/vukhacky_tactics.hl";;
flyspeck_needs "packing/marchal_cells.hl";;
flyspeck_needs "packing/EMNWUUS.hl";;
flyspeck_needs "packing/marchal_cells_2.hl";;
flyspeck_needs "packing/marchal_cells_2_new.hl";;
flyspeck_needs "packing/URRPHBZ1.hl";;
flyspeck_needs "packing/LEPJBDJ.hl";;
flyspeck_needs "packing/HDTFNFZ.hl";;
flyspeck_needs "packing/RVFXZBU.hl";;
flyspeck_needs "packing/SLTSTLO.hl";;
flyspeck_needs "packing/URRPHBZ2.hl";;
flyspeck_needs "packing/URRPHBZ3.hl";;
flyspeck_needs "packing/YNHYJIT.hl";;
flyspeck_needs "packing/NJIUTIU.hl";;
flyspeck_needs "packing/TEZFFSK.hl";;
flyspeck_needs "packing/QZKSYKG.hl";;
flyspeck_needs "packing/DDZUPHJ.hl";;
flyspeck_needs "packing/AJRIPQN.hl";;
flyspeck_needs "jordan/parse_ext_override_interface.hl";;
flyspeck_needs "jordan/real_ext.hl";;
flyspeck_needs "packing/QZYZMJC.hl";;
flyspeck_needs "packing/UPFZBZM_support_lemmas.hl";;
flyspeck_needs "packing/marchal_cells_3.hl";; 
flyspeck_needs "packing/GRUTOTI.hl";; 

(* ================  Currently added - 14 May 2012 ================== *)

flyspeck_needs "packing/sum_beta_bump.hl";; 
flyspeck_needs "packing/KIZHLTL.hl.hl";; 
flyspeck_needs "packing/sum_gammaX_lmfun_estimate.hl";; 
flyspeck_needs "packing/UPFZBZM.hl";; 
flyspeck_needs "packing/RDWKARC.hl";; 


open Sphere;;
open Euler_main_theorem;;
open Pack_defs;;
open Pack_concl;; 
open Pack1;;
open Pack2;;
open Packing3;;
open Rogers;; 
open Vukhacky_tactics;;
open Marchal_cells;;
open Emnwuus;;
open Marchal_cells_2;;
open Marchal_cells_2_new;;
open Urrphbz1;;
open Lepjbdj;;
open Hdtfnfz;;
open Rvfxzbu;;
open Sltstlo;;
open Urrphbz2;;
open Urrphbz3;;
open Ynhyjit;;
open Njiutiu;;
open Tezffsk;;
open Qzksykg;;
open Ddzuphj;;
open Ajripqn;;
open Qzyzmjc;;
open Upfzbzm_support_lemmas;;
open Marchal_cells_3;;
open Grutoti;;
open Sum_beta_bump;;

loads "/home/vu/flyspeck/working/KIZHLTL.hl";;