aboutsummaryrefslogtreecommitdiff
path: root/scratch.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* Decided on a new proper scheme for type rules using the idea of implicit ↵Josh Chen2018-06-171-0/+24
well-formed contexts and guaranteed conclusion well-formedness. Product type rules now follow this scheme.