(* ==== 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";;