aboutsummaryrefslogtreecommitdiff
path: root/spartan/lib/More_Types.thy (follow)
Commit message (Collapse)AuthorAgeFilesLines
* 1. Type-checking/inference now more principled, and the implementation is ↵Josh Chen2020-07-211-13/+17
| | | | better. 2. Changed most tactics to context tactics.
* Non-annotated object lambdaJosh Chen2020-07-091-6/+6
|
* 1. Initial `Definition` keyword. 2. ifelse.Josh Chen2020-07-081-4/+46
|
* rename foldersJosh Chen2020-06-151-0/+104