aboutsummaryrefslogtreecommitdiff
path: root/HoTT_Typing.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Put typing functionality into a .thy and clean up antiquotations, which resul...Josh Chen2019-02-111-0/+169