Diffusion Isabelle 5de9a5fbf2ec

adjustments for fewer WO assumptions
5de9a5fbf2ec
Actions

Tags

None

Subscribers

None

Description

adjustments for fewer WO assumptions

Details

Provenance

paulson <lp15@cam.ac.uk>

Authored on

Parents

rISABELLEcf8399df4d76: elimination of some needless assumptions

Branches

Unknown

Tags

Unknown

Event Timeline

paulson <lp15@cam.ac.uk> committed rISABELLE5de9a5fbf2ec: adjustments for fewer WO assumptions.Aug 9 2020, 4:18 PM

Changes (3)

Path

Size

src/

HOL/

Cardinals/

Cardinal_Order_Relation.thy

Ordinal_Arithmetic.thy

Wellorder_Constructions.thy

rISABELLE5de9a5fbf2ec

src/HOL/Cardinals/Cardinal_Order_Relation.thy

Loading...

src/HOL/Cardinals/Ordinal_Arithmetic.thy

Loading...

src/HOL/Cardinals/Wellorder_Constructions.thy

Loading...