https://github.com/jaycech3n/Isabelle-HoTT
Revision ff5454812f9e2720bd90c3a5437505644f63b487 authored by Josh Chen on 31 July 2020, 12:56:24 UTC, committed by Josh Chen on 31 July 2020, 12:56:24 UTC
. spartan/core/goals.ML . spartan/core/elaboration.ML . spartan/core/elaborated_statement.ML (FEAT) More context tacticals and search tacticals. . spartan/core/context_tactical.ML (FEAT) Improved subgoal focus. Moves fully elaborated assumptions into the context (MINOR INCOMPATIBILITY). . spartan/core/focus.ML (FIX) Normalize facts in order to be able to resolve properly. . spartan/core/typechecking.ML (MAIN) New definitions. (MAIN) Renamed theories and theorems. (MAIN) Refactor theories to fit new features.
1 parent 2b0e14b
Tip revision: ff5454812f9e2720bd90c3a5437505644f63b487 authored by Josh Chen on 31 July 2020, 12:56:24 UTC
(FEAT) Term elaboration of assumption and goal statements.
(FEAT) Term elaboration of assumption and goal statements.
Tip revision: ff54548
| File | Mode | Size |
|---|---|---|
| .github | ||
| hott | ||
| spartan | ||
| .gitignore | -rw-r--r-- | 27 bytes |
| LICENSE | -rw-r--r-- | 9.7 KB |
| README.md | -rw-r--r-- | 2.1 KB |
| ROOT | -rw-r--r-- | 850 bytes |
Computing file changes ...
