1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
6 (* Author: Thomas C. Hales *)
7 (* Date: Feb 14, 2010 *)
8 (* ========================================================================== *)
14 module type Khejkci_type = sig
15 val KHEJKCI_concl: term
20 module Khejkci : Khejkci_type = struct
22 let KHEJKCI_concl = `!V k ul. saturated V /\ packing V /\ vor_list V k ul ==>
23 ((voronoi_list V ul) face_of (voronoi_closed V (HD ul)) )`;;