Diffusion Isabelle 0135a0c77b64

tuned proofs --- avoid 'guess';
0135a0c77b64
Actions

Tags

None

Subscribers

None

Description

tuned proofs --- avoid 'guess';

Details

Provenance

Authored on

Parents

rISABELLE9e71155e3666: grant access to sun.tools.jconsole, as required for Java 17;

Branches

Unknown

Tags

Unknown

Event Timeline

makarius committed rISABELLE0135a0c77b64: tuned proofs --- avoid 'guess';.Sep 24 2021, 10:23 PM

Changes (32)

Path

Size

src/

HOL/

Analysis/

Abstract_Topology_2.thy

Binary_Product_Measure.thy

Bochner_Integration.thy

Borel_Space.thy

Caratheodory.thy

Complete_Measure.thy

Finite_Product_Measure.thy

Gamma_Function.thy

Interval_Integral.thy

Measure_Space.thy

Nonnegative_Lebesgue_Integration.thy

Radon_Nikodym.thy

Set_Integral.thy

Sigma_Algebra.thy

Summation_Tests.thy

Combinatorics/

Multiset_Permutations.thy

Complex_Analysis/

Complex_Residues.thy

Computational_Algebra/

Factorial_Ring.thy

Formal_Power_Series.thy

Normalized_Fraction.thy

Polynomial_Factorial.thy

Number_Theory/

Residue_Primitive_Roots.thy

Probability/

Discrete_Topology.thy

Independent_Family.thy

Information.thy

Probability_Measure.thy

Projective_Limit.thy

Stopping_Time.thy

rISABELLE0135a0c77b64

src/HOL/Analysis/Abstract_Topology_2.thy

Loading...

src/HOL/Analysis/Binary_Product_Measure.thy

Loading...

src/HOL/Analysis/Bochner_Integration.thy

Loading...

src/HOL/Analysis/Borel_Space.thy

Loading...

src/HOL/Analysis/Caratheodory.thy

Loading...

src/HOL/Analysis/Complete_Measure.thy

Loading...

src/HOL/Analysis/Finite_Product_Measure.thy

Loading...

src/HOL/Analysis/Gamma_Function.thy

Loading...

src/HOL/Analysis/Interval_Integral.thy

Loading...

src/HOL/Analysis/Measure_Space.thy

Loading...

src/HOL/Analysis/Nonnegative_Lebesgue_Integration.thy

Loading...

src/HOL/Analysis/Radon_Nikodym.thy

Loading...

src/HOL/Analysis/Regularity.thy

Loading...

src/HOL/Analysis/Set_Integral.thy

Loading...

src/HOL/Analysis/Sigma_Algebra.thy

Loading...

src/HOL/Analysis/Summation_Tests.thy

Loading...

src/HOL/Combinatorics/Multiset_Permutations.thy

Loading...

src/HOL/Complex_Analysis/Complex_Residues.thy

Loading...

src/HOL/Computational_Algebra/Factorial_Ring.thy

Loading...

src/HOL/Computational_Algebra/Formal_Power_Series.thy

Loading...

src/HOL/Computational_Algebra/Normalized_Fraction.thy

Loading...

src/HOL/Computational_Algebra/Polynomial.thy

Loading...

src/HOL/Computational_Algebra/Polynomial_Factorial.thy

Loading...

src/HOL/Number_Theory/Residue_Primitive_Roots.thy

Loading...

src/HOL/Probability/Discrete_Topology.thy

Loading...

src/HOL/Probability/Fin_Map.thy

Loading...

src/HOL/Probability/Independent_Family.thy

Loading...

src/HOL/Probability/Information.thy

Loading...

src/HOL/Probability/Levy.thy

Loading...

src/HOL/Probability/Probability_Measure.thy

Loading...

src/HOL/Probability/Projective_Limit.thy

Loading...

src/HOL/Probability/Stopping_Time.thy

Loading...