top: THEORY %------------------------------------------------------------------------ % Elementary properties of reals and operations over reals % % top_sigma -- provides a family of summation functions % over functions [T FROM int -> real] % product_real -- defines product over functions [int -> real] % bounded_reals -- defines sup, inf, max, min % real_sets -- properties of sup, inf, max, min % abs_lems -- additional properties of abs % exponent_props -- additional properties of expt % sqrt -- properties of square root % sqrt_approx -- definitions of sqrt_newton and sqrt_bisect % (newton and bisection methods for computing square roots). % sqrt_rew -- for (AUTO-REWRITE-THEORY "sqrt_rew") % sq -- square function and properties % sqrt_ax -- old version of square root % % CHANGES: % % 4/4/01: % real_facts -- MOVED TO analysis library % real_fun_ops -- MOVED TO analysis library % real_fun_props -- MOVED TO analysis library % % 8/1/01: % sqrt_exists -- existence proof of sqrt % sqrt_approx -- theory added (by Fleuriot/Geser) % % 8/7/01 % sigma_with, sigma_zero added to sigma % % 10/3/01 % real_facts -- DUPLICATED FROM analysis library % real_fun_ops -- DUPLICATED FROM analysis library %------------------------------------------------------------------------ BEGIN IMPORTING top_sigma, product_real, bounded_reals, real_fun_ops, real_sets, real_fun_props, abs_lems, exponent_props, sqrt, sqrt_approx, sqrt_rew, sqrt_ax END top