(* ========================================================================== *) (* FLYSPECK - BOOK FORMALIZATION *) (* *) (* Definition: NOPZSEH *) (* Chapter: Packing *) (* Author: Thomas C. Hales *) (* Date: Feb 14, 2010 *) (* ========================================================================== *) (* In the text `vor_list` is written with a bar under `voronoi_list` bar V k *) module type Nopzseh_def_type = sig val NOPZSEH : thm end;; flyspeck_needs "general/sphere.hl";; module Nopzseh : Nopzseh_def_type = struct let NOPZSEH = Sphere.BARV;; end;;