aboutsummaryrefslogtreecommitdiff
path: root/Proj.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Refactor HoTT_Methods.thy, proved more stuff with new methods.Josh Chen2018-07-031-74/+30
* Rewrote methods: wellformed now two lines, uses named theorems. New, more pow...Josh Chen2018-07-031-27/+6
* Finished proofs of projectionsJosh Chen2018-06-301-20/+76
* Proving theorems in Proj.thy in a simpler way with wellformedJosh Chen2018-06-281-40/+23
* Move projection function definitions out of Sum.thyJosh Chen2018-06-271-0/+196