Diffusion afp-devel b4c2b0dc9ede

merged
b4c2b0dc9ede
Actions

Tags

None

Subscribers

None

Description

merged

Details

Provenance

Authored on

Parents

rAFP4f6728047f6b: weakened ordering requirements
rAFP7f2113075eaa: merge

Branches

Unknown

Tags

Unknown

Event Timeline

desharna committed rAFPb4c2b0dc9ede: merged.Nov 15 2021, 10:38 AM

Merged Changes

4f6728047f6b weakened ordering requirements
Author
desharna
Browse Repository
No Builds
No Audits
8b85f22f4dd1 used well-founded pre-order in standard redundancy criterions
Author
desharna
Browse Repository
No Builds
No Audits
edd3acfc1381 derived refutational completeness from finitary and non-finitary standard…
Author
desharna
Browse Repository
No Builds
No Audits
3dc8035b2428 added missing topics;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
3aae61bb0567 clarified hugo build signature;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
d2e0fd5a6ec2 added more steps to afp site generation tool;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
a40fc791abac tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
3e1f6e97fb35 added hugo project by Carlin MacKenzie;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
fb767a74d676 added sitegen scripts by Carlin MacKenzie (slightly tweaked);
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
9895c8d9135b added afp hugo module;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
17494afe4715 clarified afp_dependencies: proper typed output;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
d08381f4f088 Added afp structure module;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
2272fe40054f Added python wrapper;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
bb594d6d379d clarified metadata;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
8225e73dbf62 tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
153b52d5a513 added afp hugo component;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
22ee7f2dcda1 added afp python component with required packages;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
4f170b69e2da merged;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
061880a9cd9e feat(afp/tools): added initial site build tool
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
ead6c0ad1a67 tuned(afp/tools): metadata sorted
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
fa45268f13d7 tuned(afp/tools): tuned parser/unparser
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
88ca579ca6cd feat(afp/tools): more metadata and toml conversion;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
a3eb648b93ca feat(afp/tools): added TOML lexer and parser;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
d6535281a69a tuned(afp/tools): module jar locations;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
70ac60fa1e2d fix(afp/tools): added missing metadata, improved toml structure
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
49990125bc11 fix(afp/tools): removed TOML formatting heuristics for simplicity;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
88d0e6a26ce1 feat(afp/tools): added TOML module;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
02bc4563612a feat(afp/tools): added metadata migration tool;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
12c42ff80fc6 feat(afp/tools): migrated scala tool_bodys to proper tools;
Author
Fabian Huch <huch@in.tum.de>
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 (94)

Path

Size

doc/

editors/

metadata/

templates/

Algebraic_Numbers

Algebraic_Number_Tests.thy

Algebraic_Numbers.thy

Algebraic_Numbers_Prelim.thy

Complex_Algebraic_Numbers.thy

Real_Algebraic_Numbers.thy

Real_Factorization.thy

Cubic_Quartic_Equations

Complex_Roots.thy

Min_Int_Poly_Complex_Impl.thy

Factor_Algebraic_Polynomial

Factor_Complex_Poly.thy

Factor_Real_Poly.thy

Is_Int_To_Int.thy

MPoly_Container.thy

MPoly_Divide.thy

MPoly_Divide_Code.thy

Multivariate_Resultant.thy

Poly_Connection.thy

Roots_of_Algebraic_Poly.thy

Roots_of_Algebraic_Poly_Impl.thy

Roots_of_Real_Complex_Poly.thy

Roots_via_IA.thy

Linear_Recurrences/

Solver/

Linear_Recurrences_Solver.thy

Szemeredi_Regularity

Word_Lib/

Bit_Comprehension.thy

Machine_Word_32.thy

Most_significant_bit.thy

Signed_Words.thy

Word_Lemmas.thy

Word_Lib_Sumo.thy

Amicable_Numbers.html

Aristotles_Assertoric_Syllogistic.html

Complete_Non_Orders.html

Conditional_Transfer_Rule.html

Cubic_Quartic_Equations.html

Dirichlet_L.html

Factor_Algebraic_Polynomial.html

Finitely_Generated_Abelian_Groups.html

Girth_Chromatic.html

Hermite_Lindemann.html

Irrational_Series_Erdos_Straus.html

Irrationality_J_Hancl.html

Real_Power.html

Schutz_Spacetime.html

Szemeredi_Regularity.html

Transcendence_Series_Hancl_Rucki.html

Types_To_Sets_Extension.html

statistics.html

rAFPb4c2b0dc9ede

doc/editors/web.md

Loading...

metadata/metadata

Loading...

metadata/templates/about.tpl

Loading...

thys/Algebraic_Numbers/Algebraic_Number_Tests.thy

Loading...

thys/Algebraic_Numbers/Algebraic_Numbers.thy

Loading...

thys/Algebraic_Numbers/Algebraic_Numbers_Prelim.thy

Loading...

thys/Algebraic_Numbers/Complex_Algebraic_Numbers.thy

Loading...

thys/Algebraic_Numbers/ROOT

Loading...

thys/Algebraic_Numbers/Real_Algebraic_Numbers.thy

Loading...

thys/Algebraic_Numbers/Real_Factorization.thy

Loading...

thys/Algebraic_Numbers/Real_Roots.thy

Loading...

thys/Cubic_Quartic_Equations/Complex_Roots.thy

Loading...

thys/Cubic_Quartic_Equations/Min_Int_Poly_Complex_Impl.thy

Loading...

thys/Cubic_Quartic_Equations/ROOT

Loading...

thys/Factor_Algebraic_Polynomial/Factor_Complex_Poly.thy

Loading...

thys/Factor_Algebraic_Polynomial/Factor_Real_Poly.thy

Loading...

thys/Factor_Algebraic_Polynomial/Is_Int_To_Int.thy

Loading...

thys/Factor_Algebraic_Polynomial/MPoly_Container.thy

Loading...

thys/Factor_Algebraic_Polynomial/MPoly_Divide.thy

Loading...

thys/Factor_Algebraic_Polynomial/MPoly_Divide_Code.thy

Loading...

thys/Factor_Algebraic_Polynomial/Multivariate_Resultant.thy

Loading...

thys/Factor_Algebraic_Polynomial/Poly_Connection.thy

Loading...

thys/Factor_Algebraic_Polynomial/ROOT

Loading...

thys/Factor_Algebraic_Polynomial/Roots_of_Algebraic_Poly.thy

Loading...

thys/Factor_Algebraic_Polynomial/Roots_of_Algebraic_Poly_Impl.thy

Loading...

thys/Factor_Algebraic_Polynomial/Roots_of_Real_Complex_Poly.thy

Loading...

thys/Factor_Algebraic_Polynomial/Roots_via_IA.thy

Loading...

thys/Factor_Algebraic_Polynomial/document/root.bib

Loading...

thys/Factor_Algebraic_Polynomial/document/root.tex

Loading...

thys/Linear_Recurrences/ROOT

Loading...

thys/Linear_Recurrences/Solver/Linear_Recurrences_Solver.thy

Loading...

thys/PAL/PAL.thy

Loading...

thys/PAL/ROOT

Loading...

thys/PAL/document/root.bib

Loading...

thys/PAL/document/root.tex

Loading...

thys/ROOTS

Loading...

thys/Real_Power/Log.thy

Loading...

thys/Real_Power/ROOT

Loading...

thys/Real_Power/RatPower.thy

Loading...

thys/Real_Power/RealPower.thy

Loading...

thys/Real_Power/document/root.tex

Loading...

thys/Szemeredi_Regularity/ROOT

Loading...

thys/Szemeredi_Regularity/Szemeredi.thy

Loading...

thys/Szemeredi_Regularity/document/root.bib

Loading...

thys/Szemeredi_Regularity/document/root.tex

Loading...

thys/Word_Lib/Aligned.thy

Loading...

thys/Word_Lib/Bit_Comprehension.thy

Loading...

thys/Word_Lib/Bits_Int.thy

Loading...

thys/Word_Lib/Guide.thy

Loading...

thys/Word_Lib/Machine_Word_32.thy

Loading...

thys/Word_Lib/Most_significant_bit.thy

Loading...

thys/Word_Lib/Signed_Words.thy

Loading...

thys/Word_Lib/Word_EqI.thy

Loading...

thys/Word_Lib/Word_Lemmas.thy

Loading...

thys/Word_Lib/Word_Lib_Sumo.thy

Loading...

web/about.html

Loading...

web/entries/Amicable_Numbers.html

Loading...

web/entries/Aristotles_Assertoric_Syllogistic.html

Loading...

web/entries/Complete_Non_Orders.html

Loading...

web/entries/Conditional_Transfer_Rule.html

Loading...

web/entries/Cubic_Quartic_Equations.html

Loading...

web/entries/Dirichlet_L.html

Loading...

web/entries/Factor_Algebraic_Polynomial.html

Loading...

web/entries/Finitely_Generated_Abelian_Groups.html

Loading...

web/entries/Girth_Chromatic.html

Loading...

web/entries/Green.html

Loading...

web/entries/Hermite_Lindemann.html

Loading...

web/entries/Irrational_Series_Erdos_Straus.html

Loading...

web/entries/Irrationality_J_Hancl.html

Loading...

web/entries/Octonions.html

Loading...

web/entries/PAL.html

Loading...

web/entries/Real_Power.html

Loading...

web/entries/Schutz_Spacetime.html

Loading...

web/entries/SpecCheck.html

Loading...

web/entries/Szemeredi_Regularity.html

Loading...

web/entries/Transcendence_Series_Hancl_Rucki.html

Loading...

web/entries/Types_To_Sets_Extension.html

Loading...

web/index.html

Loading...

web/rss.xml

Loading...

web/statistics.html

Loading...

web/topics.html

Loading...