aboutsummaryrefslogtreecommitdiff
path: root/Type_Families.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* prune import listsJosh Chen2019-03-081-1/+1
* type lemmas for derived functions should type the functions themselvesJosh Chen2019-03-081-21/+88
* Make functions object-levelJosh Chen2019-03-061-27/+53
* Move definition of transport to Type_Families.thy, and change it to use meta-...Josh Chen2019-03-031-0/+115