aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Methods.thy (unfollow)
Commit message (Expand)AuthorFilesLines
2018-07-06Added attributes to type elimination rules, not sure if these will actually b...Josh Chen1-4/+43
2018-07-03Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen1-78/+14
2018-07-03Rewrote methods: wellformed now two lines, uses named theorems. New, more pow...Josh Chen1-57/+86
2018-06-30EqualityJosh Chen1-2/+12
2018-06-28wellformed method works!!!Josh Chen1-6/+6
2018-06-27wellformed method to automatically prove wellformed judgments derivable from ...Josh Chen1-0/+76