aboutsummaryrefslogtreecommitdiff
path: root/hott/List_HoTT.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Bad practice huge commit:Josh Chen2021-06-241-2/+2
* rename things + some small changesJosh Chen2021-01-311-1/+1
* Swapped notation for metas (now ?) and holes (now {}), other notation and nam...Josh Chen2021-01-181-0/+18