Diffusion afp-devel ce989c675f3a

move lemma less_multiset_doubletons
ce989c675f3a
Actions

Tags

None

Subscribers

None

Description

move lemma less_multiset_doubletons

Details

Provenance

Alexander Bentkamp <a.bentkamp@vu.nl>

Authored on

Parents

rAFPdc7cc57f1157: Lambda-free orders: restrict totality to one set

Branches

Unknown

Tags

Unknown

Event Timeline

Alexander Bentkamp <a.bentkamp@vu.nl> committed rAFPce989c675f3a: move lemma less_multiset_doubletons.Jan 28 2020, 4:48 PM

Changes (2)

Path

Size

thys/

Lambda_Free_RPOs/

Extension_Orders.thy

Nested_Multisets_Ordinals/

Multiset_More.thy

rAFPce989c675f3a

thys/Lambda_Free_RPOs/Extension_Orders.thy

Loading...

thys/Nested_Multisets_Ordinals/Multiset_More.thy

Loading...