aboutsummaryrefslogtreecommitdiff
path: root/spartan/core/tactics.ML (follow)
Commit message (Expand)AuthorAgeFilesLines
* reorganizeJosh Chen2020-08-141-1/+1
* (FEAT) Context data slots for known types and conditional type rules, as well...Josh Chen2020-08-141-8/+6
* (FEAT) Clean up typechecking/elaboration tactic: known_ctac should *solve* go...Josh Chen2020-08-091-2/+2
* (FEAT) SIDE_CONDS tactical has additional argument specifying how many initia...Josh Chen2020-08-031-8/+12
* (REF) Tweak attribute names in preparation for new logical introduction rule ...Josh Chen2020-07-311-1/+1
* (FEAT) Term elaboration of assumption and goal statements.Josh Chen2020-07-311-2/+1
* 1. Type-checking/inference now more principled, and the implementation is bet...Josh Chen2020-07-211-161/+119
* Checkpoint. THIS BUILD WILL FAILJosh Chen2020-07-161-7/+0
* reorganizeJosh Chen2020-06-191-0/+228
* reorganize folder structureJosh Chen2020-05-281-200/+0
* 1. New congruence declarations for calculational reasoning. 2. Remove old eli...Josh Chen2020-05-261-37/+4
* Reorganize theory structure. In particular, the identity type moves out from ...Josh Chen2020-05-251-0/+233
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-06 07:39:09 +0000