Diffusion afp-devel 6449004f608b

enriched abstract substitution library slightly
6449004f608b
Actions

Tags

None

Subscribers

None

Description

enriched abstract substitution library slightly

Details

Provenance

Authored on

Parents

rAFPa9b675f61a06: refactoring to make parts of proof reusable to ongoing formalization

Branches

Unknown

Tags

Unknown

Event Timeline

blanchette committed rAFP6449004f608b: enriched abstract substitution library slightly.Apr 28 2020, 9:17 AM

Changes (2)

Path

Size

thys/

Nested_Multisets_Ordinals/

Multiset_More.thy

Ordered_Resolution_Prover/

Abstract_Substitution.thy

rAFP6449004f608b

thys/Nested_Multisets_Ordinals/Multiset_More.thy

Loading...

thys/Ordered_Resolution_Prover/Abstract_Substitution.thy

Loading...