Diffusion Isabelle dd04e81172a8

nlists is picked up automatically but conflicts with the RBT setup
dd04e81172a8
Actions

Tags

None

Subscribers

None

Description

nlists is picked up automatically but conflicts with the RBT setup

Details

Provenance

Authored on

Parents

rISABELLE40e16228405e: new lemma

Branches

Unknown

Tags

Unknown

Event Timeline

nipkow committed rISABELLEdd04e81172a8: nlists is picked up automatically but conflicts with the RBT setup.Aug 11 2022, 11:57 AM

Changes (2)

Path

Size

src/

HOL/

Codegenerator_Test/

Generate_Efficient_Datastructures.thy

Library/

rISABELLEdd04e81172a8

src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy

Loading...

src/HOL/Library/NList.thy

Loading...