Diffusion afp-devel d81723aa95cb

added monotonicity lemmas of lex/mul-ext
d81723aa95cb
Actions

Tags

None

Subscribers

None

Description

added monotonicity lemmas of lex/mul-ext

Details

Provenance

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

Authored on

Parents

rAFPd8fb49658d5f: more showl-real instantiation to Show_Real thy

Branches

Unknown

Tags

Unknown

Event Timeline

Rene Thiemann <rene.thiemann@uibk.ac.at> committed rAFPd81723aa95cb: added monotonicity lemmas of lex/mul-ext.Mon, Apr 15, 4:53 PM

Changes (2)

Path

Size

thys/

Knuth_Bendix_Order/

Lexicographic_Extension.thy

Weighted_Path_Order/

Multiset_Extension2.thy

rAFPd81723aa95cb

thys/Knuth_Bendix_Order/Lexicographic_Extension.thy

Loading...

thys/Weighted_Path_Order/Multiset_Extension2.thy

Loading...