Diffusion afp-devel 2a6196e5b347

feat(Transport) add simpler function type introduction rule for extend
2a6196e5b347
Actions

Tags

None

Subscribers

None

Description

feat(Transport) add simpler function type introduction rule for extend

Details

Provenance

Authored on

Parents

rAFP237996782d80: feat(Transport) functions as binary relations, improved mono notation, make non…

Branches

Unknown

Tags

Unknown

Event Timeline

kappelmann committed rAFP2a6196e5b347: feat(Transport) add simpler function type introduction rule for extend.Sun, Apr 21, 12:33 PM

Changes (1)

Path

Size

thys/

Transport/

HOL_Basics/

Binary_Relations/

Functions/

Binary_Relations_Function_Extend.thy

rAFP2a6196e5b347

thys/Transport/HOL_Basics/Binary_Relations/Functions/Binary_Relations_Function_Extend.thy

Loading...