aboutsummaryrefslogtreecommitdiff
path: root/Equal.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen2018-07-031-1/+1
|
* Fix precedence of =Josh Chen2018-06-301-1/+1
|
* EqualityJosh Chen2018-06-301-54/+29
|
* Library organization and formattingJosh Chen2018-06-271-1/+0
|
* Type rules now have \"all\" premises explicitly stated, matching the ↵Josh Chen2018-06-121-75/+79
| | | | formulation in the HoTT book.
* Reorganize codeJosh Chen2018-06-091-0/+81