Diffusion afp-devel 87af554341ac

merge from afp-2021
87af554341ac
Actions

Tags

None

Subscribers

None

Description

merge from afp-2021

Details

Provenance

Andreas Lochbihler <mail@andreas-lochbihler.de>

Authored on

Parents

rAFP83eb79b52c4d: corrected metadata (use acute's in names of J. Divasón and René T.)
rAFPfce965a689cd: refactored and added lemma state_behaves_forward_to_backward

Branches

Unknown

Tags

Unknown

Event Timeline

Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFP87af554341ac: merge from afp-2021.Mar 15 2021, 8:59 PM

Merged Changes

This commit merges a very large number of changes. Only the first 50 are shown.

fce965a689cd refactored and added lemma state_behaves_forward_to_backward
Author
desharna
Browse Repository
No Builds
No Audits
1335f4299090 avoid name clash
Author
florian.haftmann
Browse Repository
No Builds
No Audits
1a42ddd5dbbc adapted to LuaLaTeX according to Isabelle/299f6a8faccc;
Author
makarius
Browse Repository
No Builds
No Audits
2961a61999bd reduced dependencies on List_Permutation
Author
florian.haftmann
Browse Repository
No Builds
No Audits
18cd8aa0ceae follow corresponding precedence on sets
Author
florian.haftmann
Browse Repository
No Builds
No Audits
48319c117066 consolidated names
Author
florian.haftmann
Browse Repository
No Builds
No Audits
b6ad06ee02b5 reduced dependencies on theory List_Permutation
Author
florian.haftmann
Browse Repository
No Builds
No Audits
61ac4c954810 tuned
Author
nipkow
Browse Repository
No Builds
No Audits
f29eeda4f519 Tuned presentation of Buffon's needle
Author
pruvisto
Browse Repository
No Builds
No Audits
5638327e57df tuned
Author
nipkow
Browse Repository
No Builds
No Audits
0cbb56f4445a reduced dependencies on theory List_Permutation
Author
florian.haftmann
Browse Repository
No Builds
No Audits
de7a40fb511d tidied up messy proofs
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
7281051707f6 lemma diffusion
Author
florian.haftmann
Browse Repository
No Builds
No Audits
a41a4c9f031d more connections between mset _ = mset _ and permutations
Author
florian.haftmann
Browse Repository
No Builds
No Audits
713ce6d3becb dissolve theory with duplicated name from afp
Author
florian.haftmann
Browse Repository
No Builds
No Audits
59274460849c merge from afp-2021
Author
kleing
Browse Repository
No Builds
No Audits
ca99cb5446f9 merge from afp-2021
Author
kleing
Browse Repository
No Builds
No Audits
6137b578dc54 multiset as equivalence class of permuted lists
Author
florian.haftmann
Browse Repository
No Builds
No Audits
f7efb0c6c76f emphasize connection to multisets
Author
florian.haftmann
Browse Repository
No Builds
No Audits
3b6c0a05c5cf Updating Jinja from apply-style to Isar-style
Author
Susannah Mansky <susannahej@gmail.com>
Browse Repository
No Builds
No Audits
5c7a3b0533b3 more specific name
Author
florian.haftmann
Browse Repository
No Builds
No Audits
f92a0d6fefa1 merged
Author
makarius
Browse Repository
No Builds
No Audits
4f8e7efb12a8 adapted to Isabelle/0110e2e2964c;
Author
makarius
Browse Repository
No Builds
No Audits
be5e2dcd71e3 adapted to Isabelle/f0db1e4c89bc;
Author
makarius
Browse Repository
No Builds
No Audits
f8f24482ab45 dedicated locale for preorder and abstract bdd operation
Author
florian.haftmann
Browse Repository
No Builds
No Audits
908f7c03d556 get rid of traditional predicate
Author
florian.haftmann
Browse Repository
No Builds
No Audits
ec187af6fd41 more accurate process_result;
Author
makarius
Browse Repository
No Builds
No Audits
fedf84a4c625 adapted to Isabelle/440546ea20e6;
Author
makarius
Browse Repository
No Builds
No Audits
4b87cdc4baaf follow_on changes from Complex_Geometry
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
de4ae134bdf9 merged
Author
paulson
Browse Repository
No Builds
No Audits
ad3482c6e1ad a massive simplification, thanks to sledgehammer, etc.
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
547cd5ffe43f adapted to isabelle-dev/73253:f6bb31879698
Author
pruvisto
Browse Repository
No Builds
No Audits
3ce2153720f3 Buffons_Needle: tuned presentation
Author
pruvisto
Browse Repository
No Builds
No Audits
bcfe34497000 Ergodic_Theory: removed 'pullback_algebra'. Turns out it already exists and is…
Author
pruvisto
Browse Repository
No Builds
No Audits
158c475e011a Updating Jinja from apply-style to Isar-style
Author
Susannah Mansky <susannahej@gmail.com>
Browse Repository
No Builds
No Audits
002a907668c5 merged
Author
paulson
Browse Repository
No Builds
No Audits
c516e3b8434f removal of unnecessary and possibly harmful attributes
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
1f7a1c0d5fbb merge from afp-2021
Author
kleing
Browse Repository
No Builds
No Audits
fd1d5b3fdd7c close branch
Author
kleing
Browse Repository
No Builds
No Audits
daa87ea0470c close branch
Author
kleing
Browse Repository
No Builds
No Audits
f7321f5a8909 close branch
Author
kleing
Browse Repository
No Builds
No Audits
a040f98f10ef close branch
Author
kleing
Browse Repository
No Builds
No Audits
ff876ac75e44 close branch
Author
kleing
Browse Repository
No Builds
No Audits
a2632f50a689 Ergodic_Theory: tuned some names
Author
pruvisto
Browse Repository
No Builds
No Audits
539ea87e2f86 Ergodic_Theory: ergodicity of the shift operator
Author
pruvisto
Browse Repository
No Builds
No Audits
13ce4ece4a74 avoid hardwired document preparation;
Author
makarius
Browse Repository
No Builds
No Audits
3e4722b88fc2 Updating Jinja from apply-style to Isar-style
Author
Susannah Mansky <susannahej@gmail.com>
Browse Repository
No Builds
No Audits
a1007d72329d Updating Jinja from apply-style to Isar-style
Author
Susannah Mansky <susannahej@gmail.com>
Browse Repository
No Builds
No Audits
918ccd4df9fe Updating Jinja from apply-style to Isar-style
Author
Susannah Mansky <susannahej@gmail.com>
Browse Repository
No Builds
No Audits
3c89665fe122 Updating Jinja from apply-style to Isar-style
Author
Susannah Mansky <susannahej@gmail.com>
Browse Repository
No Builds
No Audits

Changes (109)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

metadata/

templates/

Hermite_Lindemann

Algebraic_Integer_Divisibility.thy

Complex_Lexorder.thy

Hermite_Lindemann.thy

Min_Int_Poly.thy

More_Algebraic_Numbers_HLW.thy

More_Multivariate_Polynomial_HLW.thy

More_Polynomial_HLW.thy

Modular_arithmetic_LLL_and_HNF_algorithms

HNF_Mod_Det_Algorithm.thy

HNF_Mod_Det_Soundness.thy

LLL_Certification_via_HNF.thy

Matrix_Change_Row.thy

Signed_Modulo.thy

Storjohann_Impl.thy

Storjohann_Mod_Operation.thy

Uniqueness_Hermite.thy

Uniqueness_Hermite_JNF.thy

Ordinal_Partitions/

Erdos_Milner.thy

Projective_Measurements

CHSH_Inequality.thy

Linear_Algebra_Complements.thy

Projective_Measurements.thy

Erdos_Rado_Sunflower.thy

Abstract-Rewriting.html

Algebraic_Numbers.html

Berlekamp_Zassenhaus.html

Certification_Monads.html

Datatype_Order_Generator.html

DiscretePricing.html

First_Order_Terms.html

Hermite_Lindemann.html

Isabelle_Marries_Dirac.html

Jordan_Normal_Form.html

Knuth_Bendix_Order.html

LLL_Basis_Reduction.html

LLL_Factorization.html

Lifting_Definition_Option.html

Linear_Inequalities.html

Modular_arithmetic_LLL_and_HNF_algorithms.html

Partial_Function_MR.html

Perron_Frobenius.html

Pi_Transcendental.html

Polynomial_Factorization.html

Polynomial_Interpolation.html

Polynomials.html

Power_Sum_Polynomials.html

Projective_Measurements.html

Smith_Normal_Form.html

Sqrt_Babylonian.html

Stochastic_Matrices.html

Subresultants.html

Sunflowers.html

Transitive-Closure-II.html

Transitive-Closure.html

statistics.html

rAFP87af554341ac

metadata/metadata

metadata/templates/about.tpl

thys/Hermite_Lindemann/Algebraic_Integer_Divisibility.thy

thys/Hermite_Lindemann/Complex_Lexorder.thy

thys/Hermite_Lindemann/Hermite_Lindemann.thy

thys/Hermite_Lindemann/Min_Int_Poly.thy

thys/Hermite_Lindemann/Misc_HLW.thy

thys/Hermite_Lindemann/More_Algebraic_Numbers_HLW.thy

thys/Hermite_Lindemann/More_Multivariate_Polynomial_HLW.thy

thys/Hermite_Lindemann/More_Polynomial_HLW.thy

thys/Hermite_Lindemann/ROOT

thys/Hermite_Lindemann/document/root.bib

thys/Hermite_Lindemann/document/root.tex

thys/Mereology/CEM.thy

thys/Mereology/CM.thy

thys/Mereology/EM.thy

thys/Mereology/GEM.thy

thys/Mereology/GM.thy

thys/Mereology/GMM.thy

thys/Mereology/M.thy

thys/Mereology/MM.thy

thys/Mereology/PM.thy

thys/Mereology/ROOT

thys/Mereology/document/root.bib

thys/Mereology/document/root.tex

thys/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Algorithm.thy

thys/Modular_arithmetic_LLL_and_HNF_algorithms/HNF_Mod_Det_Soundness.thy

thys/Modular_arithmetic_LLL_and_HNF_algorithms/LLL_Certification_via_HNF.thy

thys/Modular_arithmetic_LLL_and_HNF_algorithms/Matrix_Change_Row.thy

thys/Modular_arithmetic_LLL_and_HNF_algorithms/ROOT

thys/Modular_arithmetic_LLL_and_HNF_algorithms/Signed_Modulo.thy

thys/Modular_arithmetic_LLL_and_HNF_algorithms/Storjohann.thy

thys/Modular_arithmetic_LLL_and_HNF_algorithms/Storjohann_Impl.thy

thys/Modular_arithmetic_LLL_and_HNF_algorithms/Storjohann_Mod_Operation.thy

thys/Modular_arithmetic_LLL_and_HNF_algorithms/Uniqueness_Hermite.thy

thys/Modular_arithmetic_LLL_and_HNF_algorithms/Uniqueness_Hermite_JNF.thy

thys/Modular_arithmetic_LLL_and_HNF_algorithms/document/root.tex

thys/Ordinal_Partitions/Erdos_Milner.thy

thys/Projective_Measurements/CHSH_Inequality.thy

thys/Projective_Measurements/Linear_Algebra_Complements.thy

thys/Projective_Measurements/Projective_Measurements.thy

thys/Projective_Measurements/ROOT

thys/Projective_Measurements/document/root.tex

thys/ROOTS

thys/Sunflowers/Erdos_Rado_Sunflower.thy

thys/Sunflowers/ROOT

thys/Sunflowers/Sunflower.thy

thys/Sunflowers/document/root.bib

thys/Sunflowers/document/root.tex

web/about.html

web/entries/Abstract-Rewriting.html

web/entries/Algebraic_Numbers.html

web/entries/AnselmGod.html

web/entries/Berlekamp_Zassenhaus.html

web/entries/Certification_Monads.html

web/entries/Datatype_Order_Generator.html

web/entries/Deriving.html

web/entries/DiscretePricing.html

web/entries/Farkas.html

web/entries/First_Order_Terms.html

web/entries/Hermite.html

web/entries/Hermite_Lindemann.html

web/entries/Isabelle_Marries_Dirac.html

web/entries/Jordan_Normal_Form.html

web/entries/Knuth_Bendix_Order.html

web/entries/LLL_Basis_Reduction.html

web/entries/LLL_Factorization.html

web/entries/Lifting_Definition_Option.html

web/entries/Linear_Inequalities.html

web/entries/Matrix.html

web/entries/Mereology.html

web/entries/Modular_arithmetic_LLL_and_HNF_algorithms.html

web/entries/Partial_Function_MR.html

web/entries/Perron_Frobenius.html

web/entries/Pi_Transcendental.html

web/entries/Polynomial_Factorization.html

web/entries/Polynomial_Interpolation.html

web/entries/Polynomials.html

web/entries/Power_Sum_Polynomials.html

web/entries/Projective_Measurements.html

web/entries/QHLProver.html

web/entries/Real_Impl.html

web/entries/Show.html

web/entries/Simplex.html

web/entries/Smith_Normal_Form.html

web/entries/Sqrt_Babylonian.html

web/entries/Stochastic_Matrices.html

web/entries/Subresultants.html

web/entries/Sunflowers.html

web/entries/Transitive-Closure-II.html

web/entries/Transitive-Closure.html

web/entries/XML.html

web/index.html

web/rss.xml

web/statistics.html

web/topics.html