Diffusion afp-devel a60ccd2e9cc6

merged from afp2021
a60ccd2e9cc6
Actions

Tags

None

Subscribers

None

Description

merged from afp2021

Details

Provenance

Andreas Lochbihler <mail@andreas-lochbihler.de>

Authored on

Parents

rAFP4e8ba94d4183: website for SpecCheck
rAFPfe45d0404b6b: Removal of unintended files

Branches

Unknown

Tags

Unknown

Event Timeline

Andreas Lochbihler <mail@andreas-lochbihler.de> committed rAFPa60ccd2e9cc6: merged from afp2021.Jul 8 2021, 8:58 PM

Merged Changes

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

fe45d0404b6b Removal of unintended files
Author
Susannah Mansky <susannahej@gmail.com>
Browse Repository
No Builds
No Audits
6de5937fcbcb Hidden.thy to Isar
Author
Susannah Mansky <susannahej@gmail.com>
Browse Repository
No Builds
No Audits
a3060bc70b44 merged
Author
desharna
Browse Repository
No Builds
No Audits
975b2b1d8a19 renamed hide_lams opaque_lifting
Author
desharna
Browse Repository
No Builds
No Audits
805ab069d5b3 merged
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
869efd0ea35a jenkins: pre/post-hook results
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
00b5c6a1f1dd changed to opaque_lifiting as suggested by Isabelle/Jenkins
Author
yonoteam <jonjulian23@gmail.com>
Browse Repository
No Builds
No Audits
f6308605d678 changed hide_lams for opaque_lifting as suggested by Isabelle/Jenkins
Author
yonoteam <jonjulian23@gmail.com>
Browse Repository
No Builds
No Audits
9c417896a51d Added missing Public_Announcement_Logic to ROOTS file
Author
pruvisto
Browse Repository
No Builds
No Audits
9070c70617f5 More Support on Clean Syntax, Basic Lens Support, New Examples.
Author
Burkhart Wolff <wolff@lri.fr>
Browse Repository
No Builds
No Audits
2ccc185fdaac finishing arg -> Arg and moving some material out of…
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
510c4df209cf arg -> Arg: the last holdout
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
0a3968ac9ac6 merged
Author
paulson
Browse Repository
No Builds
No Audits
76eb5ab42012 arg -> Arg
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
3e122937ba1a Add entry public announcement logic
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
718cb448a456 merged
Author
Andreas Lochbihler <mail@andreas-lochbihler.de>
Browse Repository
No Builds
No Audits
20bc49db635f adapt to changes in HOL-Library.Cardinality
Author
Andreas Lochbihler <mail@andreas-lochbihler.de>
Browse Repository
No Builds
No Audits
c4a38a2daedf Added Approximation_Algorithm for Center_Selection
Author
nipkow
Browse Repository
No Builds
No Audits
5695f90acdbf proved conditional completeness of compilation
Author
desharna
Browse Repository
No Builds
No Audits
e8af416c2e70 fixed typos
Author
nipkow
Browse Repository
No Builds
No Audits
1a99ac2d4342 more word cleanup
Author
florian.haftmann
Browse Repository
No Builds
No Audits
f1195cc96e85 more default simp rules
Author
florian.haftmann
Browse Repository
No Builds
No Audits
9e42e0c5f9f9 some word streamlining
Author
florian.haftmann
Browse Repository
No Builds
No Audits
55af834ad1b8 made consistent again
Author
florian.haftmann
Browse Repository
No Builds
No Audits
291a8d8961b4 Fixed entry name for theories in sub-directory
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
d6c66721438d Stone_Relation_Algebras, Aggregation_Algebras: added history to metadata
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
7b56a9ce5619 Relational_Disjoint_Set_Forests: updated metadata to reflect added theory
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
98c7aa03457d Relational_Disjoint_Set_Forests: add theory More_Disjoint_Set_Forests
Author
Walter Guttmann <walter.guttmann@canterbury.ac.nz>
Browse Repository
No Builds
No Audits
06eb6c7d6c76 lemma grooming
Author
florian.haftmann
Browse Repository
No Builds
No Audits
c2595f7c289f no duplicates of shift operations
Author
florian.haftmann
Browse Repository
No Builds
No Audits
2e179108e08f merge Jinja/Isar work
Author
kleing
Browse Repository
No Builds
No Audits
5e24878a9118 updated change history for Interpreter_Optimization
Author
desharna
Browse Repository
No Builds
No Audits
29da90822fc7 merged
Author
paulson
Browse Repository
No Builds
No Audits
a51be9ca4b87 updated, replacing axiomatizations by proper locales
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
95f457f69761 added basic blocks
Author
desharna
Browse Repository
No Builds
No Audits
0730332cf9f6 Fix typo in date
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
337ae29a0d24 Lukas Steven's changes for his fold updates
Author
nipkow
Browse Repository
No Builds
No Audits
0b37c282b057 moved more legacy to AFP
Author
florian.haftmann
Browse Repository
No Builds
No Audits
98a8bdb85f79 merge from afp-2021
Author
kleing
Browse Repository
No Builds
No Audits
7858c60cc57a merge from afp-2021
Author
kleing
Browse Repository
No Builds
No Audits
3d11d724cbb4 more specific export_files: omit recent additions ("document", "PIDE", etc.);
Author
makarius
Browse Repository
No Builds
No Audits
e2811dc54d05 grouped lemmas
Author
florian.haftmann
Browse Repository
No Builds
No Audits
fd98855f4f8e bundles for traditional infix syntax
Author
florian.haftmann
Browse Repository
No Builds
No Audits
bdcaff25a220 complement reduced to mere abbreviation
Author
florian.haftmann
Browse Repository
No Builds
No Audits
d7c3c888a331 extracted more legacy abbreviations
Author
florian.haftmann
Browse Repository
No Builds
No Audits
3ddc21f61385 max word moved to Word_Lib in AFP
Author
florian.haftmann
Browse Repository
No Builds
No Audits
aae69e3e9178 merge from afp-2021
Author
kleing
Browse Repository
No Builds
No Audits
84e7b649025b Restore deleted theorem from Szpilrajn
Author
lukasstevens
Browse Repository
No Builds
No Audits
7c0105d2d63f tuned presentation
Author
florian.haftmann
Browse Repository
No Builds
No Audits
83f656769137 adapted to devel
Author
nipkow
Browse Repository
No Builds
No Audits

Changes (103)
Show All Changes

Very Large Commit

This commit is very large. Load each file individually.

Path

Size

metadata/

BTVSubstTypingL.thy

ContextSubtypingL.thy

IVSubstTypingL.thy

Nominal-Utils.thy

Operational.thy

SubstMethods.thy

WellformedL.thy

Public_Announcement_Logic/

SpecCheck_Base.thy

configuration.ML

SpecCheck_Dynamic.thy

dynamic_construct.ML

speccheck_dynamic.ML

SpecCheck_Examples.thy

SpecCheck_Generators.thy

gen_function.ML

SpecCheck_Output_Style.thy

output_style.ML

output_style_custom.ML

output_style_perl.ML

output_style_types.ML

SpecCheck_Show.thy

SpecCheck_Shrink.thy

shrink_types.ML

speccheck_base.ML

Van_der_Waerden

Van_der_Waerden.thy

Epistemic_Logic.html

IMP_Compiler.html

Native_Word.html

Public_Announcement_Logic.html

Van_der_Waerden.html

statistics.html

rAFPa60ccd2e9cc6

metadata/metadata

thys/IMP_Compiler/Compiler.thy

thys/IMP_Compiler/Compiler2.thy

thys/IMP_Compiler/ROOT

thys/IMP_Compiler/document/root.bib

thys/IMP_Compiler/document/root.tex

thys/MiniSail/BTVSubst.thy

thys/MiniSail/BTVSubstTypingL.thy

thys/MiniSail/ContextSubtypingL.thy

thys/MiniSail/Examples.thy

thys/MiniSail/IVSubst.thy

thys/MiniSail/IVSubstTypingL.thy

thys/MiniSail/MiniSail.thy

thys/MiniSail/Nominal-Utils.thy

thys/MiniSail/Operational.thy

thys/MiniSail/RCLogic.thy

thys/MiniSail/RCLogicL.thy

thys/MiniSail/ROOT

thys/MiniSail/Safety.thy

thys/MiniSail/SubstMethods.thy

thys/MiniSail/Syntax.thy

thys/MiniSail/SyntaxL.thy

thys/MiniSail/Typing.thy

thys/MiniSail/TypingL.thy

thys/MiniSail/Wellformed.thy

thys/MiniSail/WellformedL.thy

thys/MiniSail/document/root.bib

thys/MiniSail/document/root.tex

thys/Public_Announcement_Logic/PAL.thy

thys/ROOTS

thys/SpecCheck/README.md

thys/SpecCheck/ROOT

thys/SpecCheck/SpecCheck.thy

thys/SpecCheck/SpecCheck_Base.thy

thys/SpecCheck/configuration.ML

thys/SpecCheck/document/root.tex

thys/SpecCheck/dynamic/SpecCheck_Dynamic.thy

thys/SpecCheck/dynamic/dynamic_construct.ML

thys/SpecCheck/dynamic/speccheck_dynamic.ML

thys/SpecCheck/examples/SpecCheck_Examples.thy

thys/SpecCheck/generators/SpecCheck_Generators.thy

thys/SpecCheck/generators/gen.ML

thys/SpecCheck/generators/gen_base.ML

thys/SpecCheck/generators/gen_function.ML

thys/SpecCheck/generators/gen_int.ML

thys/SpecCheck/generators/gen_real.ML

thys/SpecCheck/generators/gen_term.ML

thys/SpecCheck/generators/gen_text.ML

thys/SpecCheck/generators/gen_types.ML

thys/SpecCheck/lecker.ML

thys/SpecCheck/output_styles/SpecCheck_Output_Style.thy

thys/SpecCheck/output_styles/output_style.ML

thys/SpecCheck/output_styles/output_style_custom.ML

thys/SpecCheck/output_styles/output_style_perl.ML

thys/SpecCheck/output_styles/output_style_types.ML

thys/SpecCheck/property.ML

thys/SpecCheck/random.ML

thys/SpecCheck/show/SpecCheck_Show.thy

thys/SpecCheck/show/show.ML

thys/SpecCheck/show/show_base.ML

thys/SpecCheck/show/show_types.ML

thys/SpecCheck/shrink/SpecCheck_Shrink.thy

thys/SpecCheck/shrink/shrink.ML

thys/SpecCheck/shrink/shrink_base.ML

thys/SpecCheck/shrink/shrink_types.ML

thys/SpecCheck/speccheck.ML

thys/SpecCheck/speccheck_base.ML

thys/SpecCheck/util.ML

thys/Van_der_Waerden/Digits.thy

thys/Van_der_Waerden/ROOT

thys/Van_der_Waerden/Van_der_Waerden.thy

thys/Van_der_Waerden/document/root.bib

thys/Van_der_Waerden/document/root.tex

web/entries/Epistemic_Logic.html

web/entries/IMP_Compiler.html

web/entries/MiniSail.html

web/entries/Native_Word.html

web/entries/Nominal2.html

web/entries/Public_Announcement_Logic.html

web/entries/Show.html

web/entries/SpecCheck.html

web/entries/Van_der_Waerden.html

web/index.html

web/rss.xml

web/statistics.html

web/topics.html