aboutsummaryrefslogtreecommitdiff
path: root/Equal.thy (unfollow)
Commit message (Expand)AuthorFilesLines
2018-07-06Remove extra attributes for elimination rules, unneeded for now.Josh Chen1-2/+1
2018-07-06Added attributes to type elimination rules, not sure if these will actually b...Josh Chen1-0/+2
2018-07-03Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen1-1/+1
2018-06-30Fix precedence of =Josh Chen1-1/+1
2018-06-30EqualityJosh Chen1-54/+29
2018-06-27Library organization and formattingJosh Chen1-1/+0
2018-06-12Type rules now have \"all\" premises explicitly stated, matching the formulat...Josh Chen1-75/+79
2018-06-09Reorganize codeJosh Chen1-0/+81