aboutsummaryrefslogtreecommitdiff
path: root/spartan/core/context_tactical.ML (unfollow)
Commit message (Expand)AuthorFilesLines
2020-08-051. fix intros method. 2. Couple extra lemmas; good small test cases for norma...Josh Chen1-1/+1
2020-08-03(FEAT) SIDE_CONDS tactical has additional argument specifying how many initia...Josh Chen1-0/+4
2020-07-31(FEAT) Term elaboration of assumption and goal statements.Josh Chen1-0/+100
2020-07-211. Type-checking/inference now more principled, and the implementation is bet...Josh Chen1-5/+28
2020-07-16Checkpoint. THIS BUILD WILL FAILJosh Chen1-0/+129