Diffusion afp-devel 6f20a9c4c987

ZFC_in_HOL: Now with Cantor normal form!
6f20a9c4c987
Actions

Tags

None

Subscribers

None

Description

ZFC_in_HOL: Now with Cantor normal form!

Details

Provenance

paulson <lp15@cam.ac.uk>

Authored on

Parents

rAFP171b62f0789a: A new lemma

Branches

Unknown

Tags

Unknown

Event Timeline

paulson <lp15@cam.ac.uk> committed rAFP6f20a9c4c987: ZFC_in_HOL: Now with Cantor normal form!.Mar 17 2020, 9:39 PM

Changes (5)

Path

Size

document/

rAFP6f20a9c4c987

thys/ZFC_in_HOL/Cantor_NF.thy

Loading...

thys/ZFC_in_HOL/ROOT

Loading...

thys/ZFC_in_HOL/document/root.tex

Loading...