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