Diffusion afp-devel b07f8898e878

merge
b07f8898e878
Actions

Description

merge

Details

Provenance

Anders Schlichtkrull <andsch@cs.aau.dk>

Authored on

Parents

rAFPeaa9eb375453: small changes in FOL_Seq_Calc1 metadata
rAFP1217567e2037: merged

Branches

Unknown

Tags

Unknown

Event Timeline

Anders Schlichtkrull <andsch@cs.aau.dk> committed rAFPb07f8898e878: merge.Jul 27 2023, 4:58 AM

Merged Changes

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

eaa9eb375453 small changes in FOL_Seq_Calc1 metadata
Author
Anders Schlichtkrull <andsch@cs.aau.dk>
Browse Repository
No Builds
No Audits
20f14f9064da More Paraconsistency
Author
Anders Schlichtkrull <andsch@cs.aau.dk>
Browse Repository
No Builds
No Audits
44bccec51c26 close branch
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
9b889a22dc8c clse branch
Author
Lars Hupel <lars.hupel@mytum.de>
Browse Repository
No Builds
No Audits
4b29df4907c3 close
Author
kleing
Browse Repository
No Builds
No Audits
eff9d8ce7be8 merge closed heads
Author
kleing
Browse Repository
No Builds
No Audits
3845c7c84c17 merged via grafting
Author
kleing
Browse Repository
No Builds
No Audits
23f824709665 merged via afp-2021-1
Author
kleing
Browse Repository
No Builds
No Audits
450bdc5c8df0 updated afp sitegen doc;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
b0bf102f7744 replaced python afp stats with Isabelle/Scala tool;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
5f4c73b43f60 updated afp metadata doc (now as markdown);
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
3cf91dd7a995 afp components: removed unnecessary platforms;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
f7b9b71b4184 afp sitegen: switch to new version;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
8e3c06373cdb add sitegen ignore option;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
8c4802ca1952 improvements for toml module: proper boolean values;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
7b2fbe17e4f0 add components as proper afp deps;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
8e081a5e444f tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
882923327135 switched to standalone cross-platform afp python component;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
b88f372899cd tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
9e91b75d851a afp python build: use tgz for better cross-plattform compatability;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
8fd101fe8fd2 replaced ci_profiles by statically compiled afp_build tool (Scala 3…
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
27fff681c7f2 afp structure: added accessors;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
860c2dbfbd78 hugo site: minor changes;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
4e300068e651 merged
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
f4ad2145b146 hugo-site: improve various aspects;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
2d5998cb1410 add new authors to migration;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
d0c948a42af2 merged
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
00c034528a4a clarified formatting, for the sake of scala3;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
dbddab778577 merged
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
e3c2aeafc2c0 merged
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
fbafb44dc503 hugo site: better scrolling;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
1be19de7eecb hugo site: updated devel info;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
38314be41f9f hugo site: updated content;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
3e574f15c9bf hugo site: proper ordering;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
2ad5e37aebc5 hugo site: restricted generated affiliations;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
16c8b18bede4 hugo site: proper theory view link scrolling;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
d406e40678a5 hugo site: tuned affiliation keys;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
244ac17a6498 hugo site: proper topic-only topics page;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
fc2d817db048 hugo site: relativize paths;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
d1a781d9fb9c hugo site: list sessions separately;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
9f4523b8ed97 hugo site: tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
0f50a79d8721 hugo site: tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
79e043c174f0 hugo site: merge gen and build tool;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
e56a3c69ae27 hugo site: added doc headers;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
51c88bc0b376 hugo site: tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
8d67d9a9da75 afp metadata: index keys for emails and urls;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
e4b3556a40fe hugo site: improve theory view;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
0dd4c34b22d5 hugo site: cleaned up;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
6091eddc9db6 hugo site: added devel version;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
fef45c5031a4 hugo site: updated search and content;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits

Changes (71)

Path

Size

thys

Actuarial_Mathematics/

ROOT

CSP_RefTK/

ROOT

CZH_Foundations/

czh_sets/

CZH_Sets_BRelations.thy

CommCSL/

CommCSL.thy

Complete_Non_Orders/

Fixed_Points.thy

Conditional_Transfer_Rule/

CTR/

CTR_Postprocessing.ML

CTR_Tools/

UD/

Crypto_Standards/

DPRM_Theorem/

Diophantine/

Alpha_Sequence.thy

Floyd_Warshall/

FW_Code.thy

Forcing/

Synthetic_Definition.thy

GaleStewart_Games/

Gale_Shapley/

Gauss_Sums/

Given_Clause_Loops/

HOL-CSP/

Independence_CH/

Absolute_Versions.thy

Definitions_Main.thy

Demonstrations.thy

Forcing_Data.thy

Kappa_Closed_Notions.thy

ZF_Trans_Interpretations.thy

Khovanskii_Theorem/

Kneser_Cauchy_Davenport/

Kneser_Cauchy_Davenport_main_proofs.thy

Monad_Memo_DP/

transform/

Transform.ML

PAL/

PAL.thy

Probability_Inequality_Completeness/

ROOT

Propositional_Logic_Class/

ROOT

Real_Time_Deque/

RealTimeDeque.thy

Roth_Arithmetic_Progressions/

Roth_Arithmetic_Progressions.thy

Routing

	IpRoute_Parser.ML
	IpRoute_Parser.ml

IpRoute_Parser.ml

IpRoute_Parser.thy

Simple_Clause_Learning

Relation_Extra.thy

SCL_FOL.thy

Trail_Induced_Ordering.thy

Wellfounded_Extra.thy

SimplifiedOntologicalArgument/

KanckosLethenNo2Possibilist.thy

Transitive_Models

Cardinal_Library_Relative.thy

ROOT

	Relativization.ML
	Relativization.ml

Relativization.ml

Relativization.thy

	Relativization_Database.ML
	Relativization_Database.ml

Relativization_Database.ml

Renaming_Auto.thy

	Renaming_ML.ML
	Renaming_ML.ml

Renaming_ML.ml

	Synthetic_Definition.ML
	Synthetic_Definition.ml

Synthetic_Definition.ml

Synthetic_Definition.thy

	Utils.ML
	Utils.ml

Utils.ml

Utils.thy

Turans_Graph_Theorem/

Turan.thy

Types_To_Sets_Extension/

ETTS/

ETTS_Lemmas.ML

Youngs_Inequality/

Youngs.thy

rAFPb07f8898e878

View Options

thys/Actuarial_Mathematics/ROOT

View Options

thys/CSP_RefTK/ROOT

View Options

thys/CZH_Foundations/czh_sets/CZH_Sets_BRelations.thy

View Options

thys/CommCSL/CommCSL.thy

View Options

thys/Complete_Non_Orders/Fixed_Points.thy

View Options

thys/Conditional_Transfer_Rule/CTR/CTR_Postprocessing.ML

View Options

thys/Conditional_Transfer_Rule/CTR_Tools/CTR_Utilities.ML

View Options

thys/Conditional_Transfer_Rule/UD/UD.ML

View Options

thys/Crypto_Standards/FIPS180_4.thy

View Options

thys/Crypto_Standards/PKCS1v2_2.thy

View Options

thys/Crypto_Standards/SEC1v2_0.thy

View Options

thys/DPRM_Theorem/Diophantine/Alpha_Sequence.thy

View Options

thys/Floyd_Warshall/FW_Code.thy

View Options

thys/Forcing/Synthetic_Definition.thy

View Options

thys/GaleStewart_Games/GaleStewartGames.thy

View Options

thys/Gale_Shapley/Gale_Shapley1.thy

View Options

thys/Gauss_Sums/Polya_Vinogradov.thy

View Options

thys/Given_Clause_Loops/Prover_Queue.thy

View Options

thys/HOL-CSP/ROOT

View Options

thys/Independence_CH/Absolute_Versions.thy

View Options

thys/Independence_CH/Definitions_Main.thy

View Options

thys/Independence_CH/Demonstrations.thy

View Options

thys/Independence_CH/Forcing_Data.thy

View Options

thys/Independence_CH/Kappa_Closed_Notions.thy

View Options

thys/Independence_CH/ZF_Trans_Interpretations.thy

View Options

thys/Intro_Dest_Elim/IDE.ML

View Options

thys/Intro_Dest_Elim/IDE_Tools/IDE_Tools.thy

View Options

thys/Intro_Dest_Elim/IDE_Tools/IDE_Utilities.ML

View Options

thys/Intro_Dest_Elim/IHOL_IDE.thy

View Options

thys/Intro_Dest_Elim/ROOT

View Options

thys/Khovanskii_Theorem/Khovanskii.thy

View Options

thys/Kneser_Cauchy_Davenport/Kneser_Cauchy_Davenport_main_proofs.thy

View Options

thys/Monad_Memo_DP/transform/Transform.ML

View Options

thys/PAL/PAL.thy

View Options

thys/Probability_Inequality_Completeness/ROOT

View Options

thys/Propositional_Logic_Class/ROOT

View Options

thys/Real_Time_Deque/RealTimeDeque.thy

View Options

thys/Roth_Arithmetic_Progressions/Roth_Arithmetic_Progressions.thy

View Options

thys/Routing/IpRoute_Parser.ML

View Options

thys/Routing/IpRoute_Parser.ml

View Options

thys/Routing/IpRoute_Parser.thy

View Options

thys/Simple_Clause_Learning/Relation_Extra.thy

View Options

thys/Simple_Clause_Learning/SCL_FOL.thy

View Options

thys/Simple_Clause_Learning/Trail_Induced_Ordering.thy

View Options

thys/Simple_Clause_Learning/Wellfounded_Extra.thy

View Options

thys/SimplifiedOntologicalArgument/KanckosLethenNo2Possibilist.thy

View Options

thys/Transitive_Models/Cardinal_Library_Relative.thy

View Options

thys/Transitive_Models/ROOT

View Options

thys/Transitive_Models/Relativization.ML

View Options

thys/Transitive_Models/Relativization.ml

View Options

thys/Transitive_Models/Relativization.thy

View Options

thys/Transitive_Models/Relativization_Database.ML

View Options

thys/Transitive_Models/Relativization_Database.ml

View Options

thys/Transitive_Models/Renaming_Auto.thy

View Options

thys/Transitive_Models/Renaming_ML.ML

View Options

thys/Transitive_Models/Renaming_ML.ml

View Options

thys/Transitive_Models/Synthetic_Definition.ML

View Options

thys/Transitive_Models/Synthetic_Definition.ml

View Options

thys/Transitive_Models/Synthetic_Definition.thy

View Options

thys/Transitive_Models/Utils.ML

View Options

thys/Transitive_Models/Utils.ml

View Options

thys/Transitive_Models/Utils.thy

View Options

thys/Turans_Graph_Theorem/Turan.thy

View Options

thys/Types_To_Sets_Extension/ETTS/ETTS_Lemmas.ML

View Options

thys/Youngs_Inequality/Youngs.thy

mergeb07f8898e878Actions

Description

Details

Event Timeline

Merged Changes

Changes (71)

rAFPb07f8898e878

thys/Actuarial_Mathematics/ROOT

thys/CSP_RefTK/ROOT

thys/CZH_Foundations/czh_sets/CZH_Sets_BRelations.thy

thys/CommCSL/CommCSL.thy

thys/Complete_Non_Orders/Fixed_Points.thy

thys/Conditional_Transfer_Rule/CTR/CTR_Postprocessing.ML

thys/Conditional_Transfer_Rule/CTR_Tools/CTR_Utilities.ML

thys/Conditional_Transfer_Rule/UD/UD.ML

thys/Crypto_Standards/FIPS180_4.thy

thys/Crypto_Standards/PKCS1v2_2.thy

thys/Crypto_Standards/SEC1v2_0.thy

thys/DPRM_Theorem/Diophantine/Alpha_Sequence.thy

thys/Floyd_Warshall/FW_Code.thy

thys/Forcing/Synthetic_Definition.thy

thys/GaleStewart_Games/GaleStewartGames.thy

thys/Gale_Shapley/Gale_Shapley1.thy

thys/Gauss_Sums/Polya_Vinogradov.thy

thys/Given_Clause_Loops/Prover_Queue.thy

thys/HOL-CSP/ROOT

thys/Independence_CH/Absolute_Versions.thy

thys/Independence_CH/Definitions_Main.thy

thys/Independence_CH/Demonstrations.thy

thys/Independence_CH/Forcing_Data.thy

thys/Independence_CH/Kappa_Closed_Notions.thy

thys/Independence_CH/ZF_Trans_Interpretations.thy

thys/Intro_Dest_Elim/IDE.ML

thys/Intro_Dest_Elim/IDE_Tools/IDE_Tools.thy

thys/Intro_Dest_Elim/IDE_Tools/IDE_Utilities.ML

thys/Intro_Dest_Elim/IHOL_IDE.thy

thys/Intro_Dest_Elim/ROOT

thys/Khovanskii_Theorem/Khovanskii.thy

thys/Kneser_Cauchy_Davenport/Kneser_Cauchy_Davenport_main_proofs.thy

thys/Monad_Memo_DP/transform/Transform.ML

thys/PAL/PAL.thy

thys/Probability_Inequality_Completeness/ROOT

thys/Propositional_Logic_Class/ROOT

thys/Real_Time_Deque/RealTimeDeque.thy

thys/Roth_Arithmetic_Progressions/Roth_Arithmetic_Progressions.thy

thys/Routing/IpRoute_Parser.ML

thys/Routing/IpRoute_Parser.ml

thys/Routing/IpRoute_Parser.thy

thys/Simple_Clause_Learning/Relation_Extra.thy

thys/Simple_Clause_Learning/SCL_FOL.thy

thys/Simple_Clause_Learning/Trail_Induced_Ordering.thy

thys/Simple_Clause_Learning/Wellfounded_Extra.thy

thys/SimplifiedOntologicalArgument/KanckosLethenNo2Possibilist.thy

thys/Transitive_Models/Cardinal_Library_Relative.thy

thys/Transitive_Models/ROOT

thys/Transitive_Models/Relativization.ML

thys/Transitive_Models/Relativization.ml

thys/Transitive_Models/Relativization.thy

thys/Transitive_Models/Relativization_Database.ML

thys/Transitive_Models/Relativization_Database.ml

thys/Transitive_Models/Renaming_Auto.thy

thys/Transitive_Models/Renaming_ML.ML

thys/Transitive_Models/Renaming_ML.ml

thys/Transitive_Models/Synthetic_Definition.ML

thys/Transitive_Models/Synthetic_Definition.ml

thys/Transitive_Models/Synthetic_Definition.thy

thys/Transitive_Models/Utils.ML

thys/Transitive_Models/Utils.ml

thys/Transitive_Models/Utils.thy

thys/Turans_Graph_Theorem/Turan.thy

thys/Types_To_Sets_Extension/ETTS/ETTS_Lemmas.ML

thys/Youngs_Inequality/Youngs.thy

merge
b07f8898e878
Actions