top: THEORY %------------------------------------------------------------------------ % % top_limits -- Limit of a functions [T -> real] at a point % top_sequence -- Limits and operations on sequences of reals % top_continuity -- Continuous functions [T -> real] % top_derivative -- Differential Calculus % top_integral -- Integral Calculus % % See top_limits, top_sequences, top_continuity, top_derivative % for summary of contents % % by Bruno Dutertre Royal Holloway & Bedford New College % Rick Butler NASA Langley Research Center % Cesar Munoz National Institute For Aerospace % David Lester Manchester University % Anthony Narkawicz NASA Langley Research Center % % Version 1.0 last modified 7/12/96 % Version 1.1 updated to PVS 2.3 8/1/2000 by Rick Butler % Version 1.2 updated to PVS 2.3 3/1/2001 by Bruno in % a slightly different way. % Bruno ELIMINATED "const_fun" and associated % conversion. Now uses prelude "K_conversion". % RWB added back "const_fun" definition to % help with upward compatibility (real_fun_ops). % % Bruno changed "below_bounded" to "bounded_below?" % and changed structure of its definition. % Bruno changed "above_bounded" to "bounded_above?" % and changed structure of its definition. % Version 1.3 Added theorem in derivatives_more 5/22/01 % Version 1.4 put back "const_fun" for PVS2.4 % Version 1.5 Used MACRO feature to rename all predicates % in real_fun_preds, adding ? to name 2/28/02 % Version 1.6 Added quadratic theory in "special_functions" 3/14/02 % Version 1.7 quadratic theory moved to reals % Version 1.8 removed open? assugmption in integral theories 4/2/03 % Version 1.9 removed duplicates with reals library 4/14/03 % Version 2.0 proved step_function_integrable? in integral_step % Version 2.1 ln_exp moved to lnexp library (12/8/03) % Version 2.2 David Lester added derivatives of inverse functions % and derivative of sqrt % Version 2.3 NAME CHANGES -- See File NAME-CHANGES.txt % Version 2.4 ADDED integral_chg_var and integral_diff_doms % Version 2.5 NAME CHANGES: continuous2 --> cont_fun % Version 2.6 moved nth_derivatives, and taylors here from series % Version 2.7 add integration_by_parts and indefinite_integral 7/20/07 % Version 2.8 metric spaces, compactness, uniform continuity % % NOTE: top_integral relies on the Di Vito strategy package % NOTE: theories named *_scaf are proof scaffolding, not intended for users %------------------------------------------------------------------------ BEGIN
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
