(* ========================================================================== *)
(* FLYSPECK - BOOK FORMALIZATION                                              *)
(*                                                                            *)
(* Definition: abc_of_quadratic                                               *)
(* Chapter: LEG                                                               *)
(* Author: Thomas C. Hales                                                    *)
(* Date: 2010-02-07                                                           *)
(* ========================================================================== *)




(*
f = \x. a x^2 + b x + c, extract a b c
*)


(* moved to sphere.hl.  This file is deprecated  *)

module type Abc_of_quadratic_def_type = sig
  val abc_of_quadratic : thm
end;;



module Abc_of_quadratic : Abc_of_quadratic_def_type = struct

 let abc_of_quadratic = 
new_definition `abc_of_quadratic f = 
  let c = f (&0) in
  let  p = f (&1) in
  let n = f (-- &1) in
  ((p + n)/(&2) - c, (p -n)/(&2), c)` ;;

end;;