|
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
IMPORTING top_limits,
top_sequences,
top_continuity,
top_metric_spaces,
top_derivative,
top_riesz_representation,
top_integral % requires Manip strategies
END top
¤ Dauer der Verarbeitung: 0.1 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
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.
|
