aboutsummaryrefslogtreecommitdiff
path: root/Type_Families.thy (unfollow)
Commit message (Expand)AuthorFilesLines
2019-03-08prune import listsJosh Chen1-1/+1
2019-03-08type lemmas for derived functions should type the functions themselvesJosh Chen1-21/+88
2019-03-06Make functions object-levelJosh Chen1-27/+53
2019-03-03Move definition of transport to Type_Families.thy, and change it to use meta-...Josh Chen1-0/+115