aboutsummaryrefslogtreecommitdiff
path: root/hott/More_Nat.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* 1. Type-checking/inference now more principled, and the implementation is ↵Josh Chen2020-07-211-3/+3
| | | | better. 2. Changed most tactics to context tactics.
* reorganizeJosh Chen2020-06-191-0/+43