aboutsummaryrefslogtreecommitdiff
path: root/EqualProps.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Added attributes to type elimination rules, not sure if these will actually b...Josh Chen2018-07-061-21/+0
* Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen2018-07-031-25/+25
* Rewrote methods: wellformed now two lines, uses named theorems. New, more pow...Josh Chen2018-07-031-30/+18
* Proving path composition. Need to set up the Simplifier to simplify applicati...Josh Chen2018-06-301-10/+28
* EqualityJosh Chen2018-06-301-0/+90