1 (* ========================================================================== *)
2 (* FLYSPECK - BOOK FORMALIZATION *)
4 (* Definition: quadratic_root_plus *)
6 (* Author: Thomas C. Hales *)
8 (* ========================================================================== *)
14 Lemmas Elementary Geometry (def:calE), RPFVZDI
18 (* deprecated. Moved to sphere.hl *)
20 module type Quadratic_root_plus_def_type = sig
21 val quadratic_root_plus : thm
26 module Quadratic_root_plus : Quadratic_root_plus_def_type = struct
28 let quadratic_root_plus =
29 new_definition `quadratic_root_plus (a, b, c) = ( -- b + sqrt(b pow 2 - &4 * a * c))/ (&2 * a)`;;