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

	Commit message (Collapse)	Author	Files	Lines
2021-01-31	rename things + some small changes	Josh Chen	1	-0/+0

2020-08-14	(FEAT) Context data slots for known types and conditional type rules, as ↵	Josh Chen	1	-1/+1
	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-21	1. Type-checking/inference now more principled, and the implementation is ↵	Josh Chen	1	-3/+3
	better. 2. Changed most tactics to context tactics.
2020-06-19	reorganize	Josh Chen	1	-2/+4

2020-06-15	rename folders	Josh Chen	1	-0/+0

2020-05-28	reorganize folder structure	Josh Chen	1	-0/+0

2020-05-25	Reorganize theory structure. In particular, the identity type moves out from ↵	Josh Chen	1	-0/+0
	under Spartan to HoTT. Spartan now only has Pi and Sigma.
2020-05-24	new work on elimination tactic	Josh Chen	1	-15/+23

2020-05-22	some tweaks and comments, in preparation for general inductive type elimination	Josh Chen	1	-0/+5

2020-04-02	Brand-spanking new version using Spartan infrastructure	Josh Chen	1	-0/+33