Diffusion Isabelle 8ed78bb0b915

Tuned some proofs in HOL-Analysis
8ed78bb0b915
Actions

Tags

None

Subscribers

None

Description

Tuned some proofs in HOL-Analysis

Details

Provenance

Authored on

Parents

rISABELLE0bbe0866b7e6: The Uniq quantifier for FOL too

Branches

Unknown

Tags

Unknown

Event Timeline

pruvisto committed rISABELLE8ed78bb0b915: Tuned some proofs in HOL-Analysis.May 14 2020, 1:44 PM

Changes (8)

Path

Size

src/

HOL/

Analysis/

Abstract_Topology.thy

Bochner_Integration.thy

Finite_Cartesian_Product.thy

Further_Topology.thy

Measure_Space.thy

Library/

Infinite_Set.thy

rISABELLE8ed78bb0b915

src/HOL/Analysis/Abstract_Topology.thy

Loading...

src/HOL/Analysis/Affine.thy

Loading...

src/HOL/Analysis/Bochner_Integration.thy

Loading...

src/HOL/Analysis/Finite_Cartesian_Product.thy

Loading...

src/HOL/Analysis/Further_Topology.thy

Loading...

src/HOL/Analysis/Measure_Space.thy

Loading...

src/HOL/Analysis/Polytope.thy

Loading...

src/HOL/Library/Infinite_Set.thy

Loading...