Diffusion afp-devel e8154678b2e1

merge from afp-2021-1
e8154678b2e1
Actions

Tags

None

Subscribers

None

Description

merge from afp-2021-1

Details

Provenance

Authored on

Parents

rAFPf57bbcb7a2a5: adjust to Isabelle2021-1-RC5
rAFPb335908ca5ac: merged

Branches

Unknown

Tags

Unknown

Event Timeline

kleing committed rAFPe8154678b2e1: merge from afp-2021-1.Dec 12 2021, 6:33 AM

Merged Changes

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

b335908ca5ac merged
Author
desharna
Browse Repository
No Builds
No Audits
1cdb95bf9f7c generalized standard formula redundancy out of standard redundancy
Author
desharna
Browse Repository
No Builds
No Audits
c2061c79823c merged
Author
makarius
Browse Repository
No Builds
No Audits
5284bc2e2dfb discontinued Parse.text;
Author
makarius
Browse Repository
No Builds
No Audits
2fdd87fc6dd7 discontinued old-style {* verbatim *} tokens;
Author
makarius
Browse Repository
No Builds
No Audits
90f5fb60422f weakened locale assumptions: wfP implies asymp
Author
desharna
Browse Repository
No Builds
No Audits
7c1a5a8e9959 Add papers to metadata.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
4c46cf956c77 refactored Standard_Redundancy_Criterion to not use ordering type classes
Author
desharna
Browse Repository
No Builds
No Audits
1ffda7071d4a isabelle update_cartouches;
Author
makarius
Browse Repository
No Builds
No Audits
d4ed7c4aca73 removed obsolete "extend" operation;
Author
makarius
Browse Repository
No Builds
No Audits
98ecfb2297ef more symbolic latex_output via XML (using YXML within text);
Author
makarius
Browse Repository
No Builds
No Audits
df2034347bc9 prefer symbolic Latex.environment (typeset in Isabelle/Scala);
Author
makarius
Browse Repository
No Builds
No Audits
0bc1235e5fb6 tuned signature;
Author
makarius
Browse Repository
No Builds
No Audits
5a8b07a912c1 feat(Auto2_HOL) fix setup such that auto2 can be used by other object logics…
Author
kappelmann
Browse Repository
No Builds
No Audits
a2b90cb55ad1 Tuned: use a star in witness.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
8dfc109e1ef5 merge from afp-2021-1
Author
kleing
Browse Repository
No Builds
No Audits
3232fddb53c7 In the definition of regular pair, switched from strict to non-strict
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
068616f9fbde Rename H to S in maximal_exactly_one.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
1266c86cf47b added loader;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
b30cbcc1846c tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
d6ff995cf5a9 tuned: more canonical Isabelle code style;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
b32649b547e9 proper loading of foundational hrefs;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
53e6f3897fff fix dependencies;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
ad7234dfa6b4 Get rid of the sat abbreviation.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
2f55c21c3d3d Add missing spaces in semantics_tm.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
9c5a5af856b8 No space in front of object-logic forall.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
5dcf43ecbb6d Non-conflicting name for boolean denotation.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
bd0387cbded7 Simpler Hintikka definition.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
7ed432999588 Add syntactic abbreviation for constants.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
ab1cf8fca876 added devel flag;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
cc835fde7a38 updated about page;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
c6cf7b096b98 fixed lemma following Isabelle/c256bba593f3
Author
desharna
Browse Repository
No Builds
No Audits
f8f7720a7451 fix dangerous context management
Author
Simon Wimmer <wimmers@in.tum.de>
Browse Repository
No Builds
No Audits
5f2eb2ceef51 moved extraction of related entries to hugo;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
a53823fdccd8 improved keyword extraction;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
cea71b734a23 added keywords to site generated entry data;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
b69b09d8f99a use tmp file for python script instead of command;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
e450d45c4680 added js-side theory loading to afp site;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
5857c4582eae integrated metadata changes into site;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
09790a81f454 added missing keyword data;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
5369b980e2fe removed html dir from sitegen (now set inside hugo);
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
c5355362ec54 tuned sitegen: moved dependencies generation to scala
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
df920a57d3cf changed generated author format;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
f09cb003fe3c tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
f69e70cf8a17 tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
2b9064e3aaa4 tuned hugo: static files more explicit;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
1fe98b11c666 A slightly stronger lemma allowing slightly simpler proofs
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
12628bcb34d2 tuned;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
29324715b4d0 proper authors/affiliations gen for hugo taxonomy;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
f81257bb1f6d clarified hugo data;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits

Changes (128)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

metadata/

Hahn_Jordan_Decomposition

Extended_Reals_Sums_Compl.thy

Hahn_Jordan_Decomposition.thy

Hahn_Jordan_Prelims.thy

SimplifiedOntologicalArgument

DisableKodkodScala.thy

KanckosLethenNo2Possibilist.thy

ScottVariant.thy

SimpleVariant.thy

SimpleVariantHF.thy

SimpleVariantPG.thy

SimpleVariantSE.thy

SimpleVariantSEinT.thy

SimplifiedOntologicalArgument.thy

UFilterVariant.thy

Van_Emde_Boas_Trees

Imperative_HOL_Time

Heap_Time_Monad.thy

Imperative_HOL_Time.thy

Separation_Logic_Imperative_HOL

Hoare_Triple.thy

Refine_Imp_Hol.thy

Imperative_HOL_Add.thy

Syntax_Match.thy

Simple_TBOUND_Cond.thy

Time_Reasoning.thy

VEBT_Bounds.thy

VEBT_BuildupMemImp.thy

VEBT_Definitions.thy

VEBT_DelImperative.thy

VEBT_Delete.thy

VEBT_DeleteBounds.thy

VEBT_DeleteCorrectness.thy

VEBT_Example.thy

VEBT_Example_Setup.thy

VEBT_Height.thy

VEBT_Insert.thy

VEBT_InsertCorrectness.thy

VEBT_Intf_Functional.thy

VEBT_Intf_Imperative.thy

VEBT_List_Assn.thy

VEBT_Member.thy

VEBT_MinMax.thy

VEBT_SuccPredImperative.thy

VEBT_Uniqueness.thy

AI_Planning_Languages_Semantics.html

Algebraic_Numbers.html

Automatic_Refinement.html

Binomial-Heaps.html

Bounded_Deducibility_Security.html

CAVA_Automata.html

CAVA_LTL_Modelchecker.html

Collections.html

Cubic_Quartic_Equations.html

DFS_Framework.html

Dijkstra_Shortest_Path.html

DiscretePricing.html

EdmondsKarp_Maxflow.html

Epistemic_Logic.html

FOL_Seq_Calc1.html

Factor_Algebraic_Polynomial.html

Finger-Trees.html

Flow_Networks.html

Floyd_Warshall.html

Hahn_Jordan_Decomposition.html

Hermite_Lindemann.html

Knuth_Morris_Pratt.html

LTL_to_GBA.html

Polynomials.html

Prim_Dijkstra_Simple.html

Priority_Search_Trees.html

Program-Conflict-Analysis.html

Projective_Measurements.html

Prpu_Maxflow.html

Public_Announcement_Logic.html

Refine_Imperative_HOL.html

Refine_Monadic.html

Separation_Logic_Imperative_HOL.html

SimplifiedOntologicalArgument.html

Tree-Automata.html

Van_Emde_Boas_Trees.html

VerifyThis2018.html

VerifyThis2019.html

statistics.html

rAFPe8154678b2e1

metadata/metadata

metadata/topics

thys/Hahn_Jordan_Decomposition/Extended_Reals_Sums_Compl.thy

thys/Hahn_Jordan_Decomposition/Hahn_Jordan_Decomposition.thy

thys/Hahn_Jordan_Decomposition/Hahn_Jordan_Prelims.thy

thys/Hahn_Jordan_Decomposition/ROOT

thys/Hahn_Jordan_Decomposition/document/root.bib

thys/Hahn_Jordan_Decomposition/document/root.tex

thys/ROOTS

thys/SimplifiedOntologicalArgument/BaseDefs.thy

thys/SimplifiedOntologicalArgument/DisableKodkodScala.thy

thys/SimplifiedOntologicalArgument/HOML.thy

thys/SimplifiedOntologicalArgument/KanckosLethenNo2Possibilist.thy

thys/SimplifiedOntologicalArgument/MFilter.thy

thys/SimplifiedOntologicalArgument/ROOT

thys/SimplifiedOntologicalArgument/ScottVariant.thy

thys/SimplifiedOntologicalArgument/SimpleVariant.thy

thys/SimplifiedOntologicalArgument/SimpleVariantHF.thy

thys/SimplifiedOntologicalArgument/SimpleVariantPG.thy

thys/SimplifiedOntologicalArgument/SimpleVariantSE.thy

thys/SimplifiedOntologicalArgument/SimpleVariantSEinT.thy

thys/SimplifiedOntologicalArgument/SimplifiedOntologicalArgument.thy

thys/SimplifiedOntologicalArgument/UFilterVariant.thy

thys/SimplifiedOntologicalArgument/document/root.bib

thys/SimplifiedOntologicalArgument/document/root.tex

thys/Van_Emde_Boas_Trees/Imperative_HOL_Time/Array_Time.thy

thys/Van_Emde_Boas_Trees/Imperative_HOL_Time/Heap.thy

thys/Van_Emde_Boas_Trees/Imperative_HOL_Time/Heap_Time_Monad.thy

thys/Van_Emde_Boas_Trees/Imperative_HOL_Time/Imperative_HOL_Time.thy

thys/Van_Emde_Boas_Trees/Imperative_HOL_Time/README

thys/Van_Emde_Boas_Trees/Imperative_HOL_Time/Ref_Time.thy

thys/Van_Emde_Boas_Trees/ROOT

thys/Van_Emde_Boas_Trees/Separation_Logic_Imperative_HOL/Assertions.thy

thys/Van_Emde_Boas_Trees/Separation_Logic_Imperative_HOL/Automation.thy

thys/Van_Emde_Boas_Trees/Separation_Logic_Imperative_HOL/Hoare_Triple.thy

thys/Van_Emde_Boas_Trees/Separation_Logic_Imperative_HOL/Refine_Imp_Hol.thy

thys/Van_Emde_Boas_Trees/Separation_Logic_Imperative_HOL/Sep_Main.thy

thys/Van_Emde_Boas_Trees/Separation_Logic_Imperative_HOL/Tools/Imperative_HOL_Add.thy

thys/Van_Emde_Boas_Trees/Separation_Logic_Imperative_HOL/Tools/Syntax_Match.thy

thys/Van_Emde_Boas_Trees/Time_Reasoning/Simple_TBOUND_Cond.thy

thys/Van_Emde_Boas_Trees/Time_Reasoning/Time_Reasoning.thy

thys/Van_Emde_Boas_Trees/VEBT_Bounds.thy

thys/Van_Emde_Boas_Trees/VEBT_BuildupMemImp.thy

thys/Van_Emde_Boas_Trees/VEBT_Definitions.thy

thys/Van_Emde_Boas_Trees/VEBT_DelImperative.thy

thys/Van_Emde_Boas_Trees/VEBT_Delete.thy

thys/Van_Emde_Boas_Trees/VEBT_DeleteBounds.thy

thys/Van_Emde_Boas_Trees/VEBT_DeleteCorrectness.thy

thys/Van_Emde_Boas_Trees/VEBT_Example.thy

thys/Van_Emde_Boas_Trees/VEBT_Example_Setup.thy

thys/Van_Emde_Boas_Trees/VEBT_Height.thy

thys/Van_Emde_Boas_Trees/VEBT_Insert.thy

thys/Van_Emde_Boas_Trees/VEBT_InsertCorrectness.thy

thys/Van_Emde_Boas_Trees/VEBT_Intf_Functional.thy

thys/Van_Emde_Boas_Trees/VEBT_Intf_Imperative.thy

thys/Van_Emde_Boas_Trees/VEBT_List_Assn.thy

thys/Van_Emde_Boas_Trees/VEBT_Member.thy

thys/Van_Emde_Boas_Trees/VEBT_MinMax.thy

thys/Van_Emde_Boas_Trees/VEBT_Pred.thy

thys/Van_Emde_Boas_Trees/VEBT_Space.thy

thys/Van_Emde_Boas_Trees/VEBT_Succ.thy

thys/Van_Emde_Boas_Trees/VEBT_SuccPredImperative.thy

thys/Van_Emde_Boas_Trees/VEBT_Uniqueness.thy

thys/Van_Emde_Boas_Trees/document/root.bib

thys/Van_Emde_Boas_Trees/document/root.tex

web/entries/AI_Planning_Languages_Semantics.html

web/entries/Algebraic_Numbers.html

web/entries/Automatic_Refinement.html

web/entries/Binomial-Heaps.html

web/entries/Bounded_Deducibility_Security.html

web/entries/CAVA_Automata.html

web/entries/CAVA_LTL_Modelchecker.html

web/entries/CoCon.html

web/entries/Collections.html

web/entries/Cubic_Quartic_Equations.html

web/entries/DFS_Framework.html

web/entries/Deriving.html

web/entries/Dijkstra_Shortest_Path.html

web/entries/DiscretePricing.html

web/entries/EdmondsKarp_Maxflow.html

web/entries/Epistemic_Logic.html

web/entries/FOL_Seq_Calc1.html

web/entries/Factor_Algebraic_Polynomial.html

web/entries/Finger-Trees.html

web/entries/Flow_Networks.html

web/entries/Floyd_Warshall.html

web/entries/Gabow_SCC.html

web/entries/Hahn_Jordan_Decomposition.html

web/entries/Hermite_Lindemann.html

web/entries/HyperCTL.html

web/entries/IMP2.html

web/entries/Knuth_Morris_Pratt.html

web/entries/Kruskal.html

web/entries/LTL_to_GBA.html

web/entries/Optics.html

web/entries/Polynomials.html

web/entries/Prim_Dijkstra_Simple.html

web/entries/Priority_Search_Trees.html

web/entries/Program-Conflict-Analysis.html

web/entries/Projective_Measurements.html

web/entries/Prpu_Maxflow.html

web/entries/Public_Announcement_Logic.html

web/entries/ROBDD.html

web/entries/Refine_Imperative_HOL.html

web/entries/Refine_Monadic.html

web/entries/Separation_Logic_Imperative_HOL.html

web/entries/SimplifiedOntologicalArgument.html

web/entries/Tree-Automata.html

web/entries/Van_Emde_Boas_Trees.html

web/entries/VerifyThis2018.html

web/entries/VerifyThis2019.html

web/index.html

web/rss.xml

web/statistics.html

web/topics.html