aboutsummaryrefslogtreecommitdiff
path: root/Sum.thy (follow)
Commit message (Expand)AuthorAgeFilesLines
* Eliminators must be completely parametrized at the meta-level.Josh Chen2018-06-171-14/+5
* projectionsJosh Chen2018-06-151-13/+28
* Type rules now have \"all\" premises explicitly stated, matching the formulat...Josh Chen2018-06-121-31/+62
* Reorganize codeJosh Chen2018-06-091-0/+78