aboutsummaryrefslogtreecommitdiff
path: root/spartan/lib (unfollow)
Commit message (Expand)AuthorFilesLines
2020-07-09Non-annotated object lambdaJosh Chen3-20/+17
2020-07-081. Initial `Definition` keyword. 2. ifelse.Josh Chen3-15/+55
2020-06-15rename foldersJosh Chen3-0/+372
2020-05-25Reorganize theory structure. In particular, the identity type moves out from ...Josh Chen10-1846/+0
2020-05-25new elimination tacticJosh Chen1-17/+65
2020-05-24new work on elimination tacticJosh Chen2-34/+85
2020-05-24small commentJosh Chen1-0/+2
2020-05-22some tweaks and comments, in preparation for general inductive type eliminationJosh Chen3-3/+7
2020-04-16update for Isabelle2020Josh Chen2-2/+2
2020-04-02Brand-spanking new version using Spartan infrastructureJosh Chen10-0/+1741