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

	Commit message (Expand)	Author	Files	Lines
2020-06-03	1. Type information context data	Josh Chen	1	-2/+3
2020-05-30	inhabitation coercion should be syntax, not logical constant!	Josh Chen	1	-2/+2
2020-05-29	fix Pi congruence rule	Josh Chen	1	-2/+2
2020-05-28	notation	Josh Chen	1	-0/+3
2020-05-28	case distinction	Josh Chen	1	-1/+5
2020-05-28	reorganize folder structure	Josh Chen	1	-14/+14
2020-05-26	1. New congruence declarations for calculational reasoning. 2. Remove old eli...	Josh Chen	1	-7/+5
2020-05-25	Lists + more reorganizing	Josh Chen	1	-2/+7
2020-05-25	Reorganize theory structure. In particular, the identity type moves out from ...	Josh Chen	1	-9/+9
2020-05-25	`refl` and `this` methods	Josh Chen	1	-8/+20
2020-05-25	new elimination tactic	Josh Chen	1	-17/+3
2020-05-24	new work on elimination tactic	Josh Chen	1	-6/+26
2020-05-22	some tweaks and comments, in preparation for general inductive type elimination	Josh Chen	1	-4/+3
2020-04-02	1. make id function an abbrev. 2. fix reduce method	Josh Chen	1	-7/+5
2020-04-02	better lambda notation	Josh Chen	1	-4/+7
2020-04-02	Brand-spanking new version using Spartan infrastructure	Josh Chen	1	-0/+463