aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Methods.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen2018-07-031-78/+14
|
* Rewrote methods: wellformed now two lines, uses named theorems. New, more ↵Josh Chen2018-07-031-57/+86
| | | | powerful derive method. Used these to rewrite proofs.
* EqualityJosh Chen2018-06-301-2/+12
|
* wellformed method works!!!Josh Chen2018-06-281-6/+6
|
* wellformed method to automatically prove wellformed judgments derivable from ↵Josh Chen2018-06-271-0/+76
a wellformed judgment