Diffusion afp-devel d54d7aa85968

fixes for compatibility with renamed / new lemmas
d54d7aa85968
Actions

Description

fixes for compatibility with renamed / new lemmas

Details

Provenance

paulson <lp15@cam.ac.uk>

Authored on

Parents

rAFP9831a6481d33: Tiny simplifications

Branches

Unknown

Tags

Unknown

Event Timeline

paulson <lp15@cam.ac.uk> committed rAFPd54d7aa85968: fixes for compatibility with renamed / new lemmas.May 25 2022, 11:54 AM

Changes (33)

Path

Size

thys/

Actuarial_Mathematics/

Preliminaries.thy

Akra_Bazzi/

Master_Theorem.thy

Buffons_Needle/

Buffons_Needle.thy

Catalan_Numbers/

Catalan_Auxiliary_Integral.thy

Catalan_Numbers.thy

Dirichlet_L/

Dirichlet_L_Functions.thy

Dirichlet_Series/

Dirichlet_Series_Analysis.thy

Error_Function/

Error_Function.thy

Error_Function_Asymptotics.thy

Euler_MacLaurin/

Fourier/

Green/

Incompleteness/

Irrationals_From_THEBOOK/

Irrationals_From_THEBOOK.thy

Ordinary_Differential_Equations/

IVP/

Upper_Lower_Solution.thy

Library/

Gronwall.thy

Vector_Derivative_On.thy

Prime_Distribution_Elementary/

Moebius_Mu_Sum.thy

Partial_Zeta_Bounds.thy

Prime_Number_Theorem/

Mertens_Theorems.thy

Newman_Ingham_Tauberian.thy

Prime_Counting_Functions.thy

Prime_Number_Theorem.thy

Prime_Number_Theorem_Library.thy

Safe_Distance/

Safe_Distance.thy

Safe_Distance_Reaction.thy

Stirling_Formula/

Gamma_Asymptotics.thy

Stirling_Formula.thy

UpDown_Scheme/

Triangular_Function.thy

Zeta_3_Irrational/

Zeta_3_Irrational.thy

Zeta_Function/

Zeta_Library.thy

rAFPd54d7aa85968

View Options

thys/Actuarial_Mathematics/Preliminaries.thy

View Options

thys/Akra_Bazzi/Master_Theorem.thy

View Options

thys/Buffons_Needle/Buffons_Needle.thy

View Options

thys/Catalan_Numbers/Catalan_Auxiliary_Integral.thy

View Options

thys/Catalan_Numbers/Catalan_Numbers.thy

View Options

thys/Dirichlet_L/Dirichlet_L_Functions.thy

View Options

thys/Dirichlet_Series/Dirichlet_Series_Analysis.thy

View Options

thys/Error_Function/Error_Function.thy

View Options

thys/Error_Function/Error_Function_Asymptotics.thy

View Options

thys/Euler_MacLaurin/Euler_MacLaurin.thy

View Options

thys/Fourier/Fourier.thy

View Options

thys/Green/Derivs.thy

View Options

thys/Green/Integrals.thy

View Options

thys/Green/Paths.thy

View Options

thys/Incompleteness/Coding.thy

View Options

thys/Irrationals_From_THEBOOK/Irrationals_From_THEBOOK.thy

View Options

thys/Ordinary_Differential_Equations/IVP/Upper_Lower_Solution.thy

View Options

thys/Ordinary_Differential_Equations/Library/Gronwall.thy

View Options

thys/Ordinary_Differential_Equations/Library/Vector_Derivative_On.thy

View Options

thys/Prime_Distribution_Elementary/Moebius_Mu_Sum.thy

View Options

thys/Prime_Distribution_Elementary/Partial_Zeta_Bounds.thy

View Options

thys/Prime_Number_Theorem/Mertens_Theorems.thy

View Options

thys/Prime_Number_Theorem/Newman_Ingham_Tauberian.thy

View Options

thys/Prime_Number_Theorem/Prime_Counting_Functions.thy

View Options

thys/Prime_Number_Theorem/Prime_Number_Theorem.thy

View Options

thys/Prime_Number_Theorem/Prime_Number_Theorem_Library.thy

View Options

thys/Safe_Distance/Safe_Distance.thy

View Options

thys/Safe_Distance/Safe_Distance_Reaction.thy

View Options

thys/Stirling_Formula/Gamma_Asymptotics.thy

View Options

thys/Stirling_Formula/Stirling_Formula.thy

View Options

thys/UpDown_Scheme/Triangular_Function.thy

View Options

thys/Zeta_3_Irrational/Zeta_3_Irrational.thy

View Options

thys/Zeta_Function/Zeta_Library.thy

fixes for compatibility with renamed / new lemmasd54d7aa85968Actions

Description

Details

Event Timeline

Changes (33)

rAFPd54d7aa85968

thys/Actuarial_Mathematics/Preliminaries.thy

thys/Akra_Bazzi/Master_Theorem.thy

thys/Buffons_Needle/Buffons_Needle.thy

thys/Catalan_Numbers/Catalan_Auxiliary_Integral.thy

thys/Catalan_Numbers/Catalan_Numbers.thy

thys/Dirichlet_L/Dirichlet_L_Functions.thy

thys/Dirichlet_Series/Dirichlet_Series_Analysis.thy

thys/Error_Function/Error_Function.thy

thys/Error_Function/Error_Function_Asymptotics.thy

thys/Euler_MacLaurin/Euler_MacLaurin.thy

thys/Fourier/Fourier.thy

thys/Green/Derivs.thy

thys/Green/Integrals.thy

thys/Green/Paths.thy

thys/Incompleteness/Coding.thy

thys/Irrationals_From_THEBOOK/Irrationals_From_THEBOOK.thy

thys/Ordinary_Differential_Equations/IVP/Upper_Lower_Solution.thy

thys/Ordinary_Differential_Equations/Library/Gronwall.thy

thys/Ordinary_Differential_Equations/Library/Vector_Derivative_On.thy

thys/Prime_Distribution_Elementary/Moebius_Mu_Sum.thy

thys/Prime_Distribution_Elementary/Partial_Zeta_Bounds.thy

thys/Prime_Number_Theorem/Mertens_Theorems.thy

thys/Prime_Number_Theorem/Newman_Ingham_Tauberian.thy

thys/Prime_Number_Theorem/Prime_Counting_Functions.thy

thys/Prime_Number_Theorem/Prime_Number_Theorem.thy

thys/Prime_Number_Theorem/Prime_Number_Theorem_Library.thy

thys/Safe_Distance/Safe_Distance.thy

thys/Safe_Distance/Safe_Distance_Reaction.thy

thys/Stirling_Formula/Gamma_Asymptotics.thy

thys/Stirling_Formula/Stirling_Formula.thy

thys/UpDown_Scheme/Triangular_Function.thy

thys/Zeta_3_Irrational/Zeta_3_Irrational.thy

thys/Zeta_Function/Zeta_Library.thy

fixes for compatibility with renamed / new lemmas
d54d7aa85968
Actions