legacy/oldpacking/packing/development/Backup/load_sequence.hl

   1
   2 (* ==== Loaded files from Vu Khac Ky - 22 Mar 2012 ========================= *)
   3
   4 #use "/usr/programs/hollight/hollight-114/hol.ml";;
   5 loads "Multivariate/flyspeck.ml";;
   6 #use "/home/vu/flyspeck/working/boot.hl";;               (* hol_version 2734 *)
   7 flyspeck_needs "trigonometry/trig1.hl";;
   8 flyspeck_needs "trigonometry/trig2.hl";;
   9 flyspeck_needs "trigonometry/euler_main_theorem.hl";;
  10 flyspeck_needs "leg/muR_def.hl";;
  11 flyspeck_needs "leg/enclosed_def.hl";;
  12 flyspeck_needs "trigonometry/trigonometry.hl";;
  13 flyspeck_needs "leg/collect_geom.hl";;
  14 flyspeck_needs "fan/fan_defs.hl";;
  15 flyspeck_needs "fan/introduction.hl";;
  16 flyspeck_needs "fan/topology.hl";;
  17 flyspeck_needs "fan/fan_misc.hl";;
  18 flyspeck_needs "fan/HypermapAndFan.hl";;
  19 flyspeck_needs "packing/pack_defs.hl";;
  20 flyspeck_needs "packing/pack_concl.hl";;
  21 flyspeck_needs "packing/pack1.hl";;
  22 flyspeck_needs "packing/pack2.hl";;
  23 flyspeck_needs "packing/pack3.hl";;
  24 flyspeck_needs "packing/Rogers.hl";;
  25 flyspeck_needs "nonlinear/vukhacky_tactics.hl";;
  26 flyspeck_needs "packing/marchal_cells.hl";;
  27 flyspeck_needs "packing/EMNWUUS.hl";;
  28 flyspeck_needs "packing/marchal_cells_2.hl";;
  29 flyspeck_needs "packing/marchal_cells_2_new.hl";;
  30 flyspeck_needs "packing/URRPHBZ1.hl";;
  31 flyspeck_needs "packing/LEPJBDJ.hl";;
  32 flyspeck_needs "packing/HDTFNFZ.hl";;
  33 flyspeck_needs "packing/RVFXZBU.hl";;
  34 flyspeck_needs "packing/SLTSTLO.hl";;
  35 flyspeck_needs "packing/URRPHBZ2.hl";;
  36 flyspeck_needs "packing/URRPHBZ3.hl";;
  37 flyspeck_needs "packing/YNHYJIT.hl";;
  38 flyspeck_needs "packing/NJIUTIU.hl";;
  39 flyspeck_needs "packing/TEZFFSK.hl";;
  40 flyspeck_needs "packing/QZKSYKG.hl";;
  41 flyspeck_needs "packing/DDZUPHJ.hl";;
  42 flyspeck_needs "packing/AJRIPQN.hl";;
  43 flyspeck_needs "jordan/parse_ext_override_interface.hl";;
  44 flyspeck_needs "jordan/real_ext.hl";;
  45 flyspeck_needs "packing/QZYZMJC.hl";;
  46 flyspeck_needs "packing/UPFZBZM_support_lemmas.hl";;
  47 flyspeck_needs "packing/marchal_cells_3.hl";;
  48 flyspeck_needs "packing/GRUTOTI.hl";;
  49
  50 (* ================  Currently added - 14 May 2012 ================== *)
  51
  52 flyspeck_needs "packing/sum_beta_bump.hl";;
  53 flyspeck_needs "packing/KIZHLTL.hl.hl";;
  54 flyspeck_needs "packing/sum_gammaX_lmfun_estimate.hl";;
  55 flyspeck_needs "packing/UPFZBZM.hl";;
  56 flyspeck_needs "packing/RDWKARC.hl";;
  57
  58
  59 open Sphere;;
  60 open Euler_main_theorem;;
  61 open Pack_defs;;
  62 open Pack_concl;;
  63 open Pack1;;
  64 open Pack2;;
  65 open Packing3;;
  66 open Rogers;;
  67 open Vukhacky_tactics;;
  68 open Marchal_cells;;
  69 open Emnwuus;;
  70 open Marchal_cells_2;;
  71 open Marchal_cells_2_new;;
  72 open Urrphbz1;;
  73 open Lepjbdj;;
  74 open Hdtfnfz;;
  75 open Rvfxzbu;;
  76 open Sltstlo;;
  77 open Urrphbz2;;
  78 open Urrphbz3;;
  79 open Ynhyjit;;
  80 open Njiutiu;;
  81 open Tezffsk;;
  82 open Qzksykg;;
  83 open Ddzuphj;;
  84 open Ajripqn;;
  85 open Qzyzmjc;;
  86 open Upfzbzm_support_lemmas;;
  87 open Marchal_cells_3;;
  88 open Grutoti;;
  89 open Sum_beta_bump;;
  90
  91 loads "/home/vu/flyspeck/working/KIZHLTL.hl";;
  92
  93