text_formalization/leg/quadratic_root_plus_def.hl

   1 (* ========================================================================== *)
   2 (* FLYSPECK - BOOK FORMALIZATION                                              *)
   3 (*                                                                            *)
   4 (* Definition: quadratic_root_plus                                            *)
   5 (* Chapter: LEG                                                               *)
   6 (* Author: Thomas C. Hales                                                    *)
   7 (* Date: 2010-02-07                                                           *)
   8 (* ========================================================================== *)
   9
  10
  11
  12
  13 (*
  14 Lemmas Elementary Geometry  (def:calE), RPFVZDI
  15 *)
  16
  17
  18 (* deprecated. Moved to sphere.hl *)
  19
  20 module type Quadratic_root_plus_def_type = sig
  21   val quadratic_root_plus : thm
  22 end;;
  23
  24
  25
  26 module Quadratic_root_plus : Quadratic_root_plus_def_type = struct
  27
  28  let quadratic_root_plus =
  29    new_definition `quadratic_root_plus (a, b, c) = ( -- b + sqrt(b pow 2 - &4 * a * c))/ (&2 * a)`;;
  30
  31 end;;
  32