legacy/oldpacking/NOPZSEH_def.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Definition: NOPZSEH                                                        *)
   5 (* Chapter: Packing                                                           *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: Feb 14, 2010                                                         *)
   8 (* ========================================================================== *)
   9
  10 (*
  11 In the text `vor_list` is written with a bar under `voronoi_list`   bar V k
  12
  13 *)
  14
  15
  16
  17 module type Nopzseh_def_type = sig
  18   val NOPZSEH : thm
  19 end;;
  20
  21 flyspeck_needs "general/sphere.hl";;
  22
  23 module Nopzseh : Nopzseh_def_type = struct
  24
  25   let NOPZSEH = Sphere.BARV;;
  26
  27 end;;