Diffusion afp-devel 65974f61a998

official fact collection sign_simps
65974f61a998
Actions

Description

official fact collection sign_simps

Details

Provenance

florian.haftmann

Authored on

Parents

rAFP415b7b57be74: dropped unused session references

Branches

Unknown

Tags

Unknown

Event Timeline

Changes (31)

Path

Size

thys/

Affine_Arithmetic/

Counterclockwise_2D_Arbitrary.thy

Executable_Euclidean_Space.thy

Count_Complex_Roots/

DiscretePricing/

Ergodic_Theory/

Gromov_Hyperbolicity/

Isometries.thy

Isometries_Classification.thy

Metric_Completion.thy

IEEE_Floating_Point/

IEEE_Properties.thy

Irrationality_J_Hancl/

Irrationality_J_Hancl.thy

LTL_Master_Theorem/

LTL_to_DRA/

DRA_Instantiation.thy

LinearQuantifierElim/

Thys/

FRE.thy

Multi_Party_Computation/

Secure_Multiplication.thy

Neumann_Morgenstern_Utility/

PMF_Composition.thy

Ordinary_Differential_Equations/

IVP/

Cones.thy

Planarity_Certificates/

Planarity/

Digraph_Map_Impl.thy

Polynomial_Interpolation/

Missing_Polynomial.thy

Missing_Unsorted.thy

Source_Coding_Theorem/

Source_Coding_Theorem.thy

Taylor_Models/

Interval.thy

Interval_Approximation.thy

Winding_Number_Eval/

Missing_Topology.thy

Winding_Number_Eval_Examples.thy

Word_Lib/

pGCL/

rAFP65974f61a998

View Options

thys/Affine_Arithmetic/Counterclockwise_2D_Arbitrary.thy

View Options

thys/Affine_Arithmetic/Executable_Euclidean_Space.thy

View Options

thys/Count_Complex_Roots/Extended_Sturm.thy

View Options

thys/DiscretePricing/CRR_Model.thy

View Options

thys/Ergodic_Theory/Fekete.thy

View Options

thys/Ergodic_Theory/Gouezel_Karlsson.thy

View Options

thys/Ergodic_Theory/Invariants.thy

View Options

thys/Gromov_Hyperbolicity/Isometries.thy

View Options

thys/Gromov_Hyperbolicity/Isometries_Classification.thy

View Options

thys/Gromov_Hyperbolicity/Metric_Completion.thy

View Options

thys/IEEE_Floating_Point/IEEE_Properties.thy

View Options

thys/Irrationality_J_Hancl/Irrationality_J_Hancl.thy

View Options

thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Instantiation.thy

View Options

thys/LinearQuantifierElim/Thys/FRE.thy

View Options

thys/Multi_Party_Computation/Secure_Multiplication.thy

View Options

thys/Neumann_Morgenstern_Utility/PMF_Composition.thy

View Options

thys/Ordinary_Differential_Equations/IVP/Cones.thy

View Options

thys/Planarity_Certificates/Planarity/Digraph_Map_Impl.thy

View Options

thys/Polynomial_Interpolation/Missing_Polynomial.thy

View Options

thys/Polynomial_Interpolation/Missing_Unsorted.thy

View Options

thys/Source_Coding_Theorem/Source_Coding_Theorem.thy

View Options

thys/Taylor_Models/Interval.thy

View Options

thys/Taylor_Models/Interval_Approximation.thy

View Options

thys/Winding_Number_Eval/Missing_Topology.thy

View Options

thys/Winding_Number_Eval/Winding_Number_Eval_Examples.thy

View Options

thys/Word_Lib/Word_Lemmas.thy

View Options

thys/pGCL/Algebra.thy

View Options

thys/pGCL/Continuity.thy

View Options

thys/pGCL/Healthiness.thy

View Options

thys/pGCL/Sublinearity.thy

View Options

official fact collection sign_simps65974f61a998Actions

Description

Details

Event Timeline

Changes (31)

rAFP65974f61a998

thys/Affine_Arithmetic/Counterclockwise_2D_Arbitrary.thy

thys/Affine_Arithmetic/Executable_Euclidean_Space.thy

thys/Count_Complex_Roots/Extended_Sturm.thy

thys/DiscretePricing/CRR_Model.thy

thys/Ergodic_Theory/Fekete.thy

thys/Ergodic_Theory/Gouezel_Karlsson.thy

thys/Ergodic_Theory/Invariants.thy

thys/Gromov_Hyperbolicity/Isometries.thy

thys/Gromov_Hyperbolicity/Isometries_Classification.thy

thys/Gromov_Hyperbolicity/Metric_Completion.thy

thys/IEEE_Floating_Point/IEEE_Properties.thy

thys/Irrationality_J_Hancl/Irrationality_J_Hancl.thy

thys/LTL_Master_Theorem/LTL_to_DRA/DRA_Instantiation.thy

thys/LinearQuantifierElim/Thys/FRE.thy

thys/Multi_Party_Computation/Secure_Multiplication.thy

thys/Neumann_Morgenstern_Utility/PMF_Composition.thy

thys/Ordinary_Differential_Equations/IVP/Cones.thy

thys/Planarity_Certificates/Planarity/Digraph_Map_Impl.thy

thys/Polynomial_Interpolation/Missing_Polynomial.thy

thys/Polynomial_Interpolation/Missing_Unsorted.thy

thys/Source_Coding_Theorem/Source_Coding_Theorem.thy

thys/Taylor_Models/Interval.thy

thys/Taylor_Models/Interval_Approximation.thy

thys/Winding_Number_Eval/Missing_Topology.thy

thys/Winding_Number_Eval/Winding_Number_Eval_Examples.thy

thys/Word_Lib/Word_Lemmas.thy

thys/pGCL/Algebra.thy

thys/pGCL/Continuity.thy

thys/pGCL/Healthiness.thy

thys/pGCL/Sublinearity.thy

thys/pGCL/WellDefined.thy

official fact collection sign_simps
65974f61a998
Actions