Diffusion Isabelle c71a44893645

eliminated one redundant proof obligation in lift_bnf for quotients
c71a44893645
Actions

Tags

None

Subscribers

None

Description

eliminated one redundant proof obligation in lift_bnf for quotients

Details

Provenance

Authored on

Parents

rISABELLE41f3ca717da5: alternative deletion in Red-Black trees

Branches

Unknown

Tags

Unknown

Event Timeline

traytel committed rISABELLEc71a44893645: eliminated one redundant proof obligation in lift_bnf for quotients.Jan 7 2020, 2:58 PM

Changes (4)

Path

Size

src/

Doc/

Datatypes/

HOL/

Datatype_Examples/

Tools/

BNF/

rISABELLEc71a44893645

src/Doc/Datatypes/Datatypes.thy

Loading...

src/HOL/Datatype_Examples/TLList.thy

Loading...

src/HOL/Quotient.thy

Loading...

src/HOL/Tools/BNF/bnf_lift.ML

Loading...