Diffusion afp-devel 3127716903da

fixes for mult_less_iff1, mult_le_cancel_iff1, mult_le_cancel_iff2
3127716903da
Actions

Description

fixes for mult_less_iff1, mult_le_cancel_iff1, mult_le_cancel_iff2

Details

Provenance

paulson <lp15@cam.ac.uk>

Authored on

Parents

rAFPe432645ba52d: patched some brittle apply-chains

Branches

Unknown

Tags

Unknown

Event Timeline

paulson <lp15@cam.ac.uk> committed rAFP3127716903da: fixes for mult_less_iff1, mult_le_cancel_iff1, mult_le_cancel_iff2.Nov 11 2020, 5:47 PM

Changes (25)

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

First_Welfare_Theorem/

Utility_Functions.thy

Fourier/

Gauss_Sums/

GenClock/

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

Matrices_for_ODEs/

MTX_Examples.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

rAFP3127716903da

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/First_Welfare_Theorem/Utility_Functions.thy

View Options

thys/Fourier/Fourier.thy

View Options

thys/Gauss_Sums/Polya_Vinogradov.thy

View Options

thys/GenClock/GenClock.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/Matrices_for_ODEs/MTX_Examples.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

fixes for mult_less_iff1, mult_le_cancel_iff1, mult_le_cancel_iff23127716903daActions

Description

Details

Event Timeline

Changes (25)

rAFP3127716903da

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/First_Welfare_Theorem/Utility_Functions.thy

thys/Fourier/Fourier.thy

thys/Gauss_Sums/Polya_Vinogradov.thy

thys/GenClock/GenClock.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/Matrices_for_ODEs/MTX_Examples.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

fixes for mult_less_iff1, mult_le_cancel_iff1, mult_le_cancel_iff2
3127716903da
Actions