Isabelle-HoTT - trying to make Isabelle/HoTT work with Isabelle 2021-1

	Commit message (Collapse)	Author	Files	Lines
2020-08-14	(FEAT) Context data slots for known types and conditional type rules, as ↵	Josh Chen	1	-1/+30
	well as a separate one for judgmental equality rules. (REF) Goal statement assumptions are now put into the new context data slots. (FEAT) `assuming` Isar keyword—like `assume` but puts assumptions into context data. (REF) Typechecking and all other tactics refactored to use type information from the context data, as opposed to looking at all facts visible in context. MINOR INCOMPATIBILITY: facts that were implicitly used in proofs now have to be annotated with [type] to make them visible throughout the context, else explicitly passed to methods via `using`, or declared with `assuming`. (REF) Fixed incompatibilities in theories.
2020-07-31	(FEAT) Term elaboration of assumption and goal statements.	Josh Chen	1	-28/+23
	. 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.
2020-07-28	small improvement	Josh Chen	1	-2/+1

2020-07-28	New `assuming` proof command for elaborated assumptions	Josh Chen	1	-64/+109

2020-07-27	Hook elaboration into assumptions mechanism	Josh Chen	1	-0/+402