Diffusion Isabelle bae4731cba8f

Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/So…
bae4731cba8f
Actions

Tags

None

Subscribers

None

Description

Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/SourceTreeTemp.14UUXO

Details

Provenance

paulson <lp15@cam.ac.uk>

Authored on

Parents

rISABELLE329cb9e6b184: A tiny bit of tidying connected with Zorn's Lemma
rISABELLE95643a0bff49: tuned;

Branches

Unknown

Tags

Unknown

Event Timeline

paulson <lp15@cam.ac.uk> committed rISABELLEbae4731cba8f: Automated merge with bundle:/var/folders/9z/l1x9y3bd16x9_70pdp4703jr0000gp/T/So….Nov 11 2021, 12:51 PM

Merged Changes

95643a0bff49 tuned;
Author
makarius
Browse Repository
No Builds
No Audits
10991d115fff tuned;
Author
makarius
Browse Repository
No Builds
No Audits
56fe200b7121 proper handling of Protocol.Export, using the payload from the message --- in…
Author
makarius
Browse Repository
No Builds
No Audits
f54c81fe84f2 revert temporary workaround 6d111935299c;
Author
makarius
Browse Repository
No Builds
No Audits
ed1e5ea25369 added lemma
Author
nipkow
Browse Repository
No Builds
No Audits
5ae76214565f merged
Author
nipkow
Browse Repository
No Builds
No Audits
1d0d6a3a3eb9 tuned attributes to avoid looping
Author
nipkow
Browse Repository
No Builds
No Audits
6e1fad4f602b added eq_iff_swap for creating symmetric variants of thms; applied it in List.
Author
nipkow
Browse Repository
No Builds
No Audits
d14918fcbd37 tuned text;
Author
makarius
Browse Repository
No Builds
No Audits
a06652d397a7 more robust timeout, following df4449c6eff1;
Author
makarius
Browse Repository
No Builds
No Audits

Changes (2)

Path

Size

src/

HOL/

rISABELLEbae4731cba8f

src/HOL/Wfrec.thy

Loading...

src/HOL/Zorn.thy

Loading...