Diffusion afp-devel b36bd29f5b14

merge
b36bd29f5b14
Actions

Description

merge

Details

Provenance

Rene Thiemann <rene.thiemann@uibk.ac.at>

Authored on

Parents

rAFPa03c4e63468f: adjusted Virtual-Substitution from 2021 to devel
rAFP7a08c3aec8d9: updated website/email address

Branches

Unknown

Tags

Unknown

Event Timeline

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPb36bd29f5b14: merge.Oct 19 2021, 4:49 PM

Merged Changes

a03c4e63468f adjusted Virtual-Substitution from 2021 to devel
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
2d64f4766089 merge of AFP 2021
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
390727e50cc9 fixed duplicate "and"
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
6e3e1e4f433c sitegen for Virtual_Substitution
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
caff571036b8 new entry: Virtual Substitution
Author
Rene Thiemann <rene.thiemann@uibk.ac.at>
Browse Repository
No Builds
No Audits
323c29c97a1e close merged branch
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
3b5ff4b8d37d Closing branch "devel"
Author
kleing
Browse Repository
No Builds
No Audits
a0d561998f20 closed branch
Author
kleing
Browse Repository
No Builds
No Audits
8e995d947fb0 closed pull-request branch
Author
Gerwin Klein <gerwin.klein@nicta.com.au>
Browse Repository
No Builds
No Audits
249c2b58d173 closed merged branch
Author
Gerwin Klein <gerwin.klein@nicta.com.au>
Browse Repository
No Builds
No Audits
ad14484777fc merged
Author
gerwin.klein@nicta.com.au
Browse Repository
No Builds
No Audits
e3e858bfc9eb merged
Author
kleing
Browse Repository
No Builds
No Audits
4bea345493dd Closed branch ltl
Author
Salomon Sickert <sickert@in.tum.de>
Browse Repository
No Builds
No Audits
53421953ad96 WIP/LTL Entry
Author
Salomon Sickert <sickert@in.tum.de>
Browse Repository
No Builds
No Audits

Changes (45)

Path

Size

metadata/

metadata

thys/

Akra_Bazzi/

Akra_Bazzi.thy

Akra_Bazzi_Asymptotics.thy

Akra_Bazzi_Library.thy

Akra_Bazzi_Method.thy

Akra_Bazzi_Real.thy

Eval_Numeral.thy

Master_Theorem.thy

Master_Theorem_Examples.thy

Bernoulli/

Bernoulli.thy

Bernoulli_FPS.thy

Periodic_Bernpoly.thy

Bertrands_Postulate/

Bertrand.thy

Buffons_Needle/

Buffons_Needle.thy

Comparison_Sort_Lower_Bound/

Comparison_Sort_Lower_Bound.thy

Descartes_Sign_Rule/

Descartes_Sign_Rule.thy

E_Transcendental/

Landau_Symbols/

Landau_Real_Products.thy

Landau_Simprocs.thy

landau_simprocs.ML

Linear_Recurrences/

Partial_Fraction_Decomposition.thy

Liouville_Numbers/

Liouville_Numbers.thy

Liouville_Numbers_Misc.thy

Minkowskis_Theorem/

Minkowskis_Theorem.thy

Myhill-Nerode/

Non_Regular_Languages.thy

Prime_Harmonic_Series/

Prime_Harmonic.thy

Prime_Harmonic_Misc.thy

Squarefree_Nat.thy

Quick_Sort_Cost/

Quick_Sort_Average_Case.thy

Randomised_Quick_Sort.thy

Random_BSTs/

Random_BSTs.thy

Randomised_Social_Choice/

Automation/

SDS_Automation.thy

Regular-Sets/

Regexp_Constructions.thy

SDS_Impossibility/

SDS_Impossibility.thy

Sturm_Sequences/

Examples/

Lib/

document/

Triangle/

rAFPb36bd29f5b14

View Options

metadata/metadata

View Options

thys/Akra_Bazzi/Akra_Bazzi.thy

View Options

thys/Akra_Bazzi/Akra_Bazzi_Asymptotics.thy

View Options

thys/Akra_Bazzi/Akra_Bazzi_Library.thy

View Options

thys/Akra_Bazzi/Akra_Bazzi_Method.thy

View Options

thys/Akra_Bazzi/Akra_Bazzi_Real.thy

View Options

thys/Akra_Bazzi/Eval_Numeral.thy

View Options

thys/Akra_Bazzi/Master_Theorem.thy

View Options

thys/Akra_Bazzi/Master_Theorem_Examples.thy

View Options

thys/Bernoulli/Bernoulli.thy

View Options

thys/Bernoulli/Bernoulli_FPS.thy

View Options

thys/Bernoulli/Periodic_Bernpoly.thy

View Options

thys/Bertrands_Postulate/Bertrand.thy

View Options

thys/Buffons_Needle/Buffons_Needle.thy

View Options

thys/Comparison_Sort_Lower_Bound/Comparison_Sort_Lower_Bound.thy

View Options

thys/Descartes_Sign_Rule/Descartes_Sign_Rule.thy

View Options

thys/E_Transcendental/E_Transcendental.thy

View Options

thys/Landau_Symbols/Group_Sort.thy

View Options

thys/Landau_Symbols/Landau_Library.thy

View Options

thys/Landau_Symbols/Landau_More.thy

View Options

thys/Landau_Symbols/Landau_Real_Products.thy

View Options

thys/Landau_Symbols/Landau_Simprocs.thy

View Options

thys/Landau_Symbols/landau_simprocs.ML

View Options

thys/Linear_Recurrences/Partial_Fraction_Decomposition.thy

View Options

thys/Liouville_Numbers/Liouville_Numbers.thy

View Options

thys/Liouville_Numbers/Liouville_Numbers_Misc.thy

View Options

thys/Minkowskis_Theorem/Minkowskis_Theorem.thy

View Options

thys/Myhill-Nerode/Non_Regular_Languages.thy

View Options

thys/Prime_Harmonic_Series/Prime_Harmonic.thy

View Options

thys/Prime_Harmonic_Series/Prime_Harmonic_Misc.thy

View Options

thys/Prime_Harmonic_Series/Squarefree_Nat.thy

View Options

thys/Quick_Sort_Cost/Quick_Sort_Average_Case.thy

View Options

thys/Quick_Sort_Cost/Randomised_Quick_Sort.thy

View Options

thys/Random_BSTs/Random_BSTs.thy

View Options

thys/Randomised_Social_Choice/Automation/SDS_Automation.thy

View Options

thys/Regular-Sets/Regexp_Constructions.thy

View Options

thys/SDS_Impossibility/SDS_Impossibility.thy

View Options

thys/Sturm_Sequences/Examples/Sturm_Ex.thy

View Options

thys/Sturm_Sequences/Lib/Misc_Polynomial.thy

View Options

thys/Sturm_Sequences/Sturm.thy

View Options

thys/Sturm_Sequences/Sturm_Method.thy

View Options

thys/Sturm_Sequences/Sturm_Theorem.thy

View Options

thys/Sturm_Sequences/document/root_userguide.tex

View Options

thys/Triangle/Angles.thy

View Options

thys/Triangle/Triangle.thy

mergeb36bd29f5b14Actions

Description

Details

Event Timeline

Merged Changes

Changes (45)

rAFPb36bd29f5b14

metadata/metadata

thys/Akra_Bazzi/Akra_Bazzi.thy

thys/Akra_Bazzi/Akra_Bazzi_Asymptotics.thy

thys/Akra_Bazzi/Akra_Bazzi_Library.thy

thys/Akra_Bazzi/Akra_Bazzi_Method.thy

thys/Akra_Bazzi/Akra_Bazzi_Real.thy

thys/Akra_Bazzi/Eval_Numeral.thy

thys/Akra_Bazzi/Master_Theorem.thy

thys/Akra_Bazzi/Master_Theorem_Examples.thy

thys/Bernoulli/Bernoulli.thy

thys/Bernoulli/Bernoulli_FPS.thy

thys/Bernoulli/Periodic_Bernpoly.thy

thys/Bertrands_Postulate/Bertrand.thy

thys/Buffons_Needle/Buffons_Needle.thy

thys/Comparison_Sort_Lower_Bound/Comparison_Sort_Lower_Bound.thy

thys/Descartes_Sign_Rule/Descartes_Sign_Rule.thy

thys/E_Transcendental/E_Transcendental.thy

thys/Landau_Symbols/Group_Sort.thy

thys/Landau_Symbols/Landau_Library.thy

thys/Landau_Symbols/Landau_More.thy

thys/Landau_Symbols/Landau_Real_Products.thy

thys/Landau_Symbols/Landau_Simprocs.thy

thys/Landau_Symbols/landau_simprocs.ML

thys/Linear_Recurrences/Partial_Fraction_Decomposition.thy

thys/Liouville_Numbers/Liouville_Numbers.thy

thys/Liouville_Numbers/Liouville_Numbers_Misc.thy

thys/Minkowskis_Theorem/Minkowskis_Theorem.thy

thys/Myhill-Nerode/Non_Regular_Languages.thy

thys/Prime_Harmonic_Series/Prime_Harmonic.thy

thys/Prime_Harmonic_Series/Prime_Harmonic_Misc.thy

thys/Prime_Harmonic_Series/Squarefree_Nat.thy

thys/Quick_Sort_Cost/Quick_Sort_Average_Case.thy

thys/Quick_Sort_Cost/Randomised_Quick_Sort.thy

thys/Random_BSTs/Random_BSTs.thy

thys/Randomised_Social_Choice/Automation/SDS_Automation.thy

thys/Regular-Sets/Regexp_Constructions.thy

thys/SDS_Impossibility/SDS_Impossibility.thy

thys/Sturm_Sequences/Examples/Sturm_Ex.thy

thys/Sturm_Sequences/Lib/Misc_Polynomial.thy

thys/Sturm_Sequences/Sturm.thy

thys/Sturm_Sequences/Sturm_Method.thy

thys/Sturm_Sequences/Sturm_Theorem.thy

thys/Sturm_Sequences/document/root_userguide.tex

thys/Triangle/Angles.thy

thys/Triangle/Triangle.thy

merge
b36bd29f5b14
Actions