aboutsummaryrefslogtreecommitdiff
path: root/ProdProps.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Moved function composition lemmas into Prod.thyJosh Chen2018-09-171-57/+0
* Some final touchups before release 0.1 for the MS thesisJosh Chen2018-09-121-1/+1
* Add the univalence axiomJosh Chen2018-09-111-0/+5
* Go back to higher-order application notationJosh Chen2018-09-111-6/+6
* Reorganize methodsJosh Chen2018-08-181-6/+6
* Regrouping type rulesJosh Chen2018-08-181-2/+1
* Misc formattingJosh Chen2018-08-181-1/+0
* Properties of function compositionJosh Chen2018-08-171-24/+5
* Partway through updating proofs after the change of the function composition ...Josh Chen2018-08-171-46/+11
* Prod.thy now has the correct definitional equality structure rule. Definition...Josh Chen2018-08-161-23/+77
* Rename to distinguish function and path composition; function composition pro...Josh Chen2018-08-151-0/+54