Diffusion Isabelle 07bec530f02e

cleaned proofs
07bec530f02e
Actions

Tags

None

Subscribers

None

Description

cleaned proofs

Details

Provenance

Authored on

Parents

rISABELLE2e8f861d21d4: redunant simp rule

Branches

Unknown

Tags

Unknown

Event Timeline

nipkow committed rISABELLE07bec530f02e: cleaned proofs.Mar 31 2020, 3:51 PM

Changes (44)

Path

Size

src/

HOL/

Analysis/

Abstract_Euclidean_Space.thy

Abstract_Topology.thy

Arcwise_Connected.thy

Ball_Volume.thy

Bochner_Integration.thy

Borel_Space.thy

Cartesian_Space.thy

Change_Of_Vars.thy

Complex_Analysis_Basics.thy

Complex_Transcendental.thy

Convex_Euclidean_Space.thy

Elementary_Metric_Spaces.thy

Elementary_Normed_Spaces.thy

Embed_Measure.thy

Equivalence_Lebesgue_Henstock_Integration.thy

Equivalence_Measurable_On_Borel.thy

Extended_Real_Limits.thy

FPS_Convergence.thy

Fashoda_Theorem.thy

Function_Metric.thy

Function_Topology.thy

Further_Topology.thy

Gamma_Function.thy

Henstock_Kurzweil_Integration.thy

Homeomorphism.thy

Improper_Integral.thy

Infinite_Set_Sum.thy

Jordan_Curve.thy

Measure_Space.thy

Nonnegative_Lebesgue_Integration.thy

Ordered_Euclidean_Space.thy

Path_Connected.thy

Product_Topology.thy

Simplex_Content.thy

Summation_Tests.thy

Tagged_Division.thy

Weierstrass_Theorems.thy

rISABELLE07bec530f02e

src/HOL/Analysis/Abstract_Euclidean_Space.thy

Loading...

src/HOL/Analysis/Abstract_Topology.thy

Loading...

src/HOL/Analysis/Arcwise_Connected.thy

Loading...

src/HOL/Analysis/Ball_Volume.thy

Loading...

src/HOL/Analysis/Bochner_Integration.thy

Loading...

src/HOL/Analysis/Borel_Space.thy

Loading...

src/HOL/Analysis/Cartesian_Space.thy

Loading...

src/HOL/Analysis/Change_Of_Vars.thy

Loading...

src/HOL/Analysis/Complex_Analysis_Basics.thy

Loading...

src/HOL/Analysis/Complex_Transcendental.thy

Loading...

src/HOL/Analysis/Convex_Euclidean_Space.thy

Loading...

src/HOL/Analysis/Cross3.thy

Loading...

src/HOL/Analysis/Derivative.thy

Loading...

src/HOL/Analysis/Elementary_Metric_Spaces.thy

Loading...

src/HOL/Analysis/Elementary_Normed_Spaces.thy

Loading...

src/HOL/Analysis/Embed_Measure.thy

Loading...

src/HOL/Analysis/Equivalence_Lebesgue_Henstock_Integration.thy

Loading...

src/HOL/Analysis/Equivalence_Measurable_On_Borel.thy

Loading...

src/HOL/Analysis/Extended_Real_Limits.thy

Loading...

src/HOL/Analysis/FPS_Convergence.thy

Loading...

src/HOL/Analysis/Fashoda_Theorem.thy

Loading...

src/HOL/Analysis/Function_Metric.thy

Loading...

src/HOL/Analysis/Function_Topology.thy

Loading...

src/HOL/Analysis/Further_Topology.thy

Loading...

src/HOL/Analysis/Gamma_Function.thy

Loading...

src/HOL/Analysis/Henstock_Kurzweil_Integration.thy

Loading...

src/HOL/Analysis/Homeomorphism.thy

Loading...

src/HOL/Analysis/Homotopy.thy

Loading...

src/HOL/Analysis/Improper_Integral.thy

Loading...

src/HOL/Analysis/Infinite_Set_Sum.thy

Loading...

src/HOL/Analysis/Jordan_Curve.thy

Loading...

src/HOL/Analysis/Lipschitz.thy

Loading...

src/HOL/Analysis/Measure_Space.thy

Loading...

src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy

Loading...

src/HOL/Analysis/Ordered_Euclidean_Space.thy

Loading...

src/HOL/Analysis/Path_Connected.thy

Loading...

src/HOL/Analysis/Polytope.thy

Loading...

src/HOL/Analysis/Product_Topology.thy

Loading...

src/HOL/Analysis/Regularity.thy

Loading...

src/HOL/Analysis/Simplex_Content.thy

Loading...

src/HOL/Analysis/Starlike.thy

Loading...

src/HOL/Analysis/Summation_Tests.thy

Loading...

src/HOL/Analysis/Tagged_Division.thy

Loading...

src/HOL/Analysis/Weierstrass_Theorems.thy

Loading...