Substantial simplification of HOL-Cardinals
f33df7529fed
Actions

Description

Substantial simplification of HOL-Cardinals

Details

Provenance

Authored on

Parents

Branches

Unknown

Tags

Unknown

Changes (6)

Path

Size

src/

HOL/

Cardinals/

rISABELLEf33df7529fed

src/HOL/Cardinals/Order_Union.thy

src/HOL/Cardinals/Ordinal_Arithmetic.thy

src/HOL/Cardinals/Wellorder_Constructions.thy

src/HOL/Cardinals/Wellorder_Embedding.thy

src/HOL/Cardinals/Wellorder_Relation.thy

Substantial simplification of HOL-Cardinalsf33df7529fedActions

Description

Details

Changes (6)

rISABELLEf33df7529fed

src/HOL/Cardinals/Order_Union.thy

src/HOL/Cardinals/Ordinal_Arithmetic.thy

src/HOL/Cardinals/Wellorder_Constructions.thy

src/HOL/Cardinals/Wellorder_Embedding.thy

src/HOL/Cardinals/Wellorder_Relation.thy

src/HOL/Relation.thy

Substantial simplification of HOL-Cardinals
f33df7529fed
Actions