Diffusion afp-devel 9b21578c2a00

New lemmas and renaming of lemmas
9b21578c2a00
Actions

Description

New lemmas and renaming of lemmas

Details

Provenance

paulson <lp15@cam.ac.uk>

Authored on

Parents

rAFPce7602a023d2: feat(ML_Unification,Transport) more robust unification + new unifiers

Branches

Unknown

Tags

Unknown

Event Timeline

paulson <lp15@cam.ac.uk> committed rAFP9b21578c2a00: New lemmas and renaming of lemmas.Feb 2 2024, 12:28 PM

Changes (24)

Path

Size

thys/

Banach_Steinhaus/

Banach_Steinhaus.thy

Banach_Steinhaus_Missing.thy

Differential_Dynamic_Logic/

Differential_Axioms.thy

Ergodic_Theory/

Gouezel_Karlsson.thy

Invariants.thy

Normalizing_Sequences.thy

Eudoxus_Reals/

Eudoxus.thy

First_Welfare_Theorem/

Utility_Functions.thy

Fourier/

Gauss_Sums/

Girth_Chromatic/

Green/

Gromov_Hyperbolicity/

Metric_Completion.thy

Interval_Arithmetic_Word32/

Interval_Word32.thy

Irrational_Series_Erdos_Straus/

Irrational_Series_Erdos_Straus.thy

LLL_Basis_Reduction/

LLL.thy

Neumann_Morgenstern_Utility/

Expected_Utility.thy

Ordinary_Differential_Equations/

Ex/

Examples_One_Step_Method.thy

Perron_Frobenius/

Perron_Frobenius.thy

Poincare_Bendixson/

Invariance.thy

QHLProver/

Quantum_Program.thy

Root_Balanced_Tree/

Root_Balanced_Tree_Tab.thy

Safe_Distance/

Safe_Distance.thy

Safe_Distance_Reaction.thy

rAFP9b21578c2a00

View Options

thys/Banach_Steinhaus/Banach_Steinhaus.thy

View Options

thys/Banach_Steinhaus/Banach_Steinhaus_Missing.thy

View Options

thys/Differential_Dynamic_Logic/Differential_Axioms.thy

View Options

thys/Ergodic_Theory/Gouezel_Karlsson.thy

View Options

thys/Ergodic_Theory/Invariants.thy

View Options

thys/Ergodic_Theory/Normalizing_Sequences.thy

View Options

thys/Eudoxus_Reals/Eudoxus.thy

View Options

thys/First_Welfare_Theorem/Utility_Functions.thy

View Options

thys/Fourier/Fourier.thy

View Options

thys/Gauss_Sums/Polya_Vinogradov.thy

View Options

thys/Girth_Chromatic/Girth_Chromatic.thy

View Options

thys/Green/CircExample.thy

View Options

thys/Gromov_Hyperbolicity/Metric_Completion.thy

View Options

thys/Interval_Arithmetic_Word32/Interval_Word32.thy

View Options

thys/Irrational_Series_Erdos_Straus/Irrational_Series_Erdos_Straus.thy

View Options

thys/LLL_Basis_Reduction/LLL.thy

View Options

thys/Neumann_Morgenstern_Utility/Expected_Utility.thy

View Options

thys/Ordinary_Differential_Equations/Ex/Examples_One_Step_Method.thy

View Options

thys/Perron_Frobenius/Perron_Frobenius.thy

View Options

thys/Poincare_Bendixson/Invariance.thy

View Options

thys/QHLProver/Quantum_Program.thy

View Options

thys/Root_Balanced_Tree/Root_Balanced_Tree_Tab.thy

View Options

thys/Safe_Distance/Safe_Distance.thy

View Options

thys/Safe_Distance/Safe_Distance_Reaction.thy

New lemmas and renaming of lemmas9b21578c2a00Actions

Description

Details

Event Timeline

Changes (24)

rAFP9b21578c2a00

thys/Banach_Steinhaus/Banach_Steinhaus.thy

thys/Banach_Steinhaus/Banach_Steinhaus_Missing.thy

thys/Differential_Dynamic_Logic/Differential_Axioms.thy

thys/Ergodic_Theory/Gouezel_Karlsson.thy

thys/Ergodic_Theory/Invariants.thy

thys/Ergodic_Theory/Normalizing_Sequences.thy

thys/Eudoxus_Reals/Eudoxus.thy

thys/First_Welfare_Theorem/Utility_Functions.thy

thys/Fourier/Fourier.thy

thys/Gauss_Sums/Polya_Vinogradov.thy

thys/Girth_Chromatic/Girth_Chromatic.thy

thys/Green/CircExample.thy

thys/Gromov_Hyperbolicity/Metric_Completion.thy

thys/Interval_Arithmetic_Word32/Interval_Word32.thy

thys/Irrational_Series_Erdos_Straus/Irrational_Series_Erdos_Straus.thy

thys/LLL_Basis_Reduction/LLL.thy

thys/Neumann_Morgenstern_Utility/Expected_Utility.thy

thys/Ordinary_Differential_Equations/Ex/Examples_One_Step_Method.thy

thys/Perron_Frobenius/Perron_Frobenius.thy

thys/Poincare_Bendixson/Invariance.thy

thys/QHLProver/Quantum_Program.thy

thys/Root_Balanced_Tree/Root_Balanced_Tree_Tab.thy

thys/Safe_Distance/Safe_Distance.thy

thys/Safe_Distance/Safe_Distance_Reaction.thy

New lemmas and renaming of lemmas
9b21578c2a00
Actions