aboutsummaryrefslogtreecommitdiff
path: root/ProdProps.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Partway through updating proofs after the change of the function composition ↵Josh Chen2018-08-171-46/+11
| | | | definition
* Prod.thy now has the correct definitional equality structure rule. ↵Josh Chen2018-08-161-23/+77
| | | | Definition of function composition and properties.
* Rename to distinguish function and path composition; function composition ↵Josh Chen2018-08-151-0/+54
proofs, which have issues...