src/HOL/Analysis/Analysis.thy
author wenzelm
Mon, 15 May 2023 14:13:58 +0200
changeset 78050 f16067da45ef
parent 77941 c35f06b0931e
child 78093 cec875dcc59e
permissions -rw-r--r--
avoid capture of inner/outer context and thus reduce heaps sizes by 20..40% (see also dd04a8b654fc, e49bf4ebf330, 9c19e15c8548, 71467e35fc3c);

theory Analysis
  imports
  (* Linear Algebra *)
  Convex
  Determinants
  (* Topology *)
  FSigma
  Sum_Topology
  Abstract_Topological_Spaces
  Connected
  Abstract_Limits
  Isolated
  (* Functional Analysis *)
  Elementary_Normed_Spaces
  Norm_Arith
  (* Vector Analysis *)
  Convex_Euclidean_Space
  Operator_Norm
  (* Unsorted *)
  Line_Segment
  Derivative
  Cartesian_Euclidean_Space
  Weierstrass_Theorems
  (* Measure and Integration Theory *)
  Ball_Volume
  Integral_Test
  Improper_Integral
  Equivalence_Measurable_On_Borel
  Lebesgue_Integral_Substitution
  Embed_Measure
  Complete_Measure
  Radon_Nikodym
  Fashoda_Theorem
  Cross3
  Homeomorphism
  Bounded_Continuous_Function
  Abstract_Topology
  Product_Topology
  Lindelof_Spaces
  Infinite_Products
  Infinite_Sum
  Infinite_Set_Sum
  Polytope
  Jordan_Curve
  Poly_Roots
  Generalised_Binomial_Theorem
  Gamma_Function
  Change_Of_Vars
  Multivariate_Analysis
  Simplex_Content
  FPS_Convergence
  Smooth_Paths
  Abstract_Euclidean_Space
  Function_Metric
begin

end