Diffusion afp-devel 3b92532c10aa

merge from afp-2021-1
3b92532c10aa
Actions

Description

merge from afp-2021-1

Details

Provenance

kleing

Authored on

Parents

rAFPd55411db27d4: only make parent dir;
rAFP7d9079a56071: regen site

Branches

Unknown

Tags

Unknown

Event Timeline

kleing committed rAFP3b92532c10aa: merge from afp-2021-1.Oct 27 2022, 1:33 AM

Merged Changes

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

af4162a23c83 Removal of some old junk
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
7af7b1ff3d02 Deleted unused material
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
ac7bd3b4f3cf nothing
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
952d8efcaef4 Instantiation of the order solver for ⊑ and ⊏ (no real effect though)
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
8d4d9ce29853 proof simplifications
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
c62e25857f9a merged
Author
paulson
Browse Repository
No Builds
No Audits
764540d3e4ce Simplified the proofs a bit
Author
paulson <lp15@cam.ac.uk>
Browse Repository
No Builds
No Audits
78c41ac583e5 merged
Author
desharna
Browse Repository
No Builds
No Audits
ab05f9116530 replaced fmember.rep_eq by fmember_iff_member_fset
Author
desharna
Browse Repository
No Builds
No Audits
5d4f4da6329f merge from afp-2021-1
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
1fea1f554ccf adapted to Isabelle/457f1cba78fb
Author
desharna
Browse Repository
No Builds
No Audits
0ea44ed00721 merged
Author
desharna
Browse Repository
No Builds
No Audits
24bae165b27b added lemmas generalizes_lit_refl[simp] and generalizes_lit_trans;
Author
desharna
Browse Repository
No Builds
No Audits
8b2af90a82ed extracted proof cases from lifting_lemma to distinct lemmas
Author
desharna
Browse Repository
No Builds
No Audits
915548bf124c tuned proof due to new simp rules
Author
nipkow
Browse Repository
No Builds
No Audits
518e0df833cd corresponding lemma was removed from distribution
Author
nipkow
Browse Repository
No Builds
No Audits
7d9079a56071 regen site
Author
kleing
Browse Repository
No Builds
No Audits
5364e7177ebe updates to BenOr_Kozen_Reif by Katherine Kosaian
Author
kleing
Browse Repository
No Builds
No Audits
33daf9a750b8 fix author entry; regen website
Author
kleing
Browse Repository
No Builds
No Audits
5e3782f5070f add change history revision
Author
kleing
Browse Repository
No Builds
No Audits
771b88d61c21 Added scene spaces, improvements to prisms, and improvements to the alphabet…
Author
Simon Foster <simon.foster@york.ac.uk>
Browse Repository
No Builds
No Audits
2b899ccfc3d6 merge from afp-2021-1
Author
kleing
Browse Repository
No Builds
No Audits
11b9a0daf6b4 remove temp file
Author
kleing
Browse Repository
No Builds
No Audits
b6f87c305821 Complex_Bounded_Operators: Various changes:
Author
kleing
Browse Repository
No Builds
No Audits
ad6ac3e1e898 slightly less abusive proof pattern
Author
florian.haftmann
Browse Repository
No Builds
No Audits
1145c2ed8f6c Many changes to entry `Complex_Bounded_Operators`:
Author
Dominique Unruh <unruh@ut.ee>
Browse Repository
No Builds
No Audits
a74db29363f5 tuned proofs
Author
florian.haftmann
Browse Repository
No Builds
No Audits
6100f6dbbfed merge from afp-2021-1
Author
kleing
Browse Repository
No Builds
No Audits
56381425e759 adjust Stalnaker_Logic to changes in Epistemic_Logic;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
474696083e43 adjusted to distribution
Author
florian.haftmann
Browse Repository
No Builds
No Audits
6fce8550ee97 remove duplicate code;
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
4c631c22d1d2 restructure afp ci builds (see Isabelle/3c4e373922ca)
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
4763f470b77d Cosmetic changes.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
d81cfd823ae9 merge from afp-2021-1
Author
Fabian Huch <huch@in.tum.de>
Browse Repository
No Builds
No Audits
a969a9029a5c clarified options, following f2094906e491;
Author
makarius
Browse Repository
No Builds
No Audits
80e872e0fe3a Comments on theories brought from ZF-Constructible. Shortening fm names
Author
sterraf
Browse Repository
No Builds
No Audits
5e7974c944c6 adjusted to distribution
Author
florian.haftmann
Browse Repository
No Builds
No Audits
2b82df697776 Remove fontenc from root.tex to make Ł show in PDF.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
189717e4b998 Update ROOT...
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
611e8be50bec Appendix with another axiom system as a variant of the proof.
Author
Asta Halkjær From <andro.from@gmail.com>
Browse Repository
No Builds
No Audits
59f623140cfa adapt to Isabelle@769a7cd5a16a
Author
kleing
Browse Repository
No Builds
No Audits
bd79c9c8cfa0 merge from afp-2021-1
Author
kleing
Browse Repository
No Builds
No Audits
b9df51ee10b8 A few more disambiguations, related to locales in CartesianCategory.
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits
3abe8bbe58c0 Merged
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits
5996c6c489c3 Further disambiguation of facts to address clashes involving ConcreteCategory…
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits
bccf6f281b7b streamlined division on polynomials
Author
florian.haftmann
Browse Repository
No Builds
No Audits
75a5ba7c00bc Complex_Bounded_Operators: Fixed errors in document generation
Author
Dominique Unruh <unruh@ut.ee>
Browse Repository
No Builds
No Audits
c51cd33d81da Complex_Bounded_Operators: Added numerous new lemmas.
Author
Dominique Unruh <unruh@ut.ee>
Browse Repository
No Builds
No Audits
2d501ecd4932 Merged
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits
47f6b2669322 Disambiguate sufficiently many facts in locales so as to permit a top-level…
Author
Eugene W. Stark <stark@cs.stonybrook.edu>
Browse Repository
No Builds
No Audits

Changes (6)

Path

Size

tools/

afp_check_metadata.scala

afp_site_gen.scala

afp_structure.scala

metadata.scala

migration/

afp_migrate_metadata.scala

toml.scala

rAFP3b92532c10aa

View Options

tools/afp_check_metadata.scala

View Options

tools/afp_site_gen.scala

View Options

tools/afp_structure.scala

View Options

tools/metadata.scala

View Options

tools/migration/afp_migrate_metadata.scala

View Options

merge from afp-2021-13b92532c10aaActions

Description

Details

Event Timeline

Merged Changes

Changes (6)

rAFP3b92532c10aa

tools/afp_check_metadata.scala

tools/afp_site_gen.scala

tools/afp_structure.scala

tools/metadata.scala

tools/migration/afp_migrate_metadata.scala

tools/toml.scala

merge from afp-2021-1
3b92532c10aa
Actions