1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Definition: abc_of_quadratic *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
14 f = \x. a x^2 + b x + c, extract a b c
18 (* moved to sphere.hl. This file is deprecated *)
20 module type Abc_of_quadratic_def_type = sig
21 val abc_of_quadratic : thm
26 module Abc_of_quadratic : Abc_of_quadratic_def_type = struct
28 let abc_of_quadratic =
29 new_definition `abc_of_quadratic f =
33 ((p + n)/(&2) - c, (p -n)/(&2), c)` ;;