legacy/oldpacking/BBDTRGC_def.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Definition: BBDTRGC                                                        *)
   5 (* Chapter: Packing                                                           *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: Feb 14, 2010                                                         *)
   8 (* ========================================================================== *)
   9
  10
  11 (*
  12 Deprecated Dec 28, 2011.
  13 Set and list versions of the Voronoi cell.  The notation in the book is overloaded.
  14 *)
  15
  16
  17 module type Bbdtrgc_def_type = sig
  18   val BBDTRGC_VORONOI_SET : thm
  19   val BBDTRGC_VORONOI_LIST : thm
  20 end;;
  21
  22 flyspeck_needs "general/sphere.hl";;
  23
  24 module Bbdtrgc : Bbdtrgc_def_type = struct
  25
  26   let BBDTRGC_VORONOI_SET = Sphere.VORONOI_SET;;
  27
  28   let BBDTRGC_VORONOI_LIST  =  Sphere.VORONOI_LIST;;
  29
  30 end;;
  31