HOL-ex.Sqrt_Script