Diffusion afp-devel 26b4f0e402c1

added lemmas on lexicographic extension
26b4f0e402c1
Actions

Tags

None

Subscribers

None

Description

added lemmas on lexicographic extension

Details

Provenance

Rene Thiemann <rene.thiemann@uibk.ac.at>

Authored on

Parents

rAFP9038bb20f96b: added code-unfold lemma

Branches

Unknown

Tags

Unknown

Event Timeline

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFP26b4f0e402c1: added lemmas on lexicographic extension.Oct 13 2023, 2:35 PM

Changes (1)

Path

Size

thys/

Knuth_Bendix_Order/

Lexicographic_Extension.thy

rAFP26b4f0e402c1

thys/Knuth_Bendix_Order/Lexicographic_Extension.thy

Loading...