legacy/oldpacking/PHZVPFY_def.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Definition: PHZVPFY                                                        *)
   5 (* Chapter: Packing                                                           *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: Feb 15, 2010                                                         *)
   8 (* ========================================================================== *)
   9
  10
  11
  12
  13
  14 module type Phzvpfy_def_type = sig
  15   val PHZVPFY : thm
  16 end;;
  17
  18 flyspeck_needs "general/sphere.hl";;
  19
  20 module Phzvpfy : Phzvpfy_def_type = struct
  21
  22  let PHZVPFY = Sphere.ROGERS;;
  23
  24 end;;
  25