tuned proofs of Equiv_Relations.equiv
c40bdfc84640
Actions

Description

tuned proofs of Equiv_Relations.equiv

Details

Provenance

Authored on

Parents

Branches

Unknown

Tags

Unknown

Changes (7)

Path

Size

src/

HOL/

Algebra/

Cardinals/

Induct/

Library/

ZF/

rISABELLEc40bdfc84640

src/HOL/Algebra/Coset.thy

src/HOL/Algebra/Sylow.thy

src/HOL/Cardinals/Wellorder_Constructions.thy

src/HOL/Induct/QuoDataType.thy

src/HOL/Induct/QuoNestedDataType.thy

src/HOL/Library/Disjoint_Sets.thy

tuned proofs of Equiv_Relations.equivc40bdfc84640Actions

Description

Details

Changes (7)

rISABELLEc40bdfc84640

src/HOL/Algebra/Coset.thy

src/HOL/Algebra/Sylow.thy

src/HOL/Cardinals/Wellorder_Constructions.thy

src/HOL/Induct/QuoDataType.thy

src/HOL/Induct/QuoNestedDataType.thy

src/HOL/Library/Disjoint_Sets.thy

src/HOL/ZF/Games.thy

tuned proofs of Equiv_Relations.equiv
c40bdfc84640
Actions