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

	Commit message (Expand)	Author	Age	Files	Lines
*	Rename to distinguish function and path composition; function composition pro...	Josh Chen	2018-08-15	1	-72/+0
*	Well-formation rules are back in the methods; new theory synthesizing the nat...	Josh Chen	2018-08-14	1	-89/+69
*	rcompose done	Josh Chen	2018-08-13	1	-33/+16
*	Commit before testing polymorphic equality eliminator	Josh Chen	2018-08-12	1	-0/+6
*	Tweaks	Josh Chen	2018-08-07	1	-0/+6
*	Old application syntax incompatible with Eisbach	Josh Chen	2018-08-07	1	-2/+2
*	Partway through changing function application syntax style.	Josh Chen	2018-08-06	1	-98/+94
*	Unit and Null types. Methods.	Josh Chen	2018-07-12	1	-16/+34
*	Pre-universe implementation commit	Josh Chen	2018-07-09	1	-20/+51
*	Added attributes to type elimination rules, not sure if these will actually b...	Josh Chen	2018-07-06	1	-1/+54
*	Refactor HoTT_Methods.thy, proved more stuff with new methods.	Josh Chen	2018-07-03	1	-18/+2
*	Decided on a new proper scheme for type rules using the idea of implicit well...	Josh Chen	2018-06-17	1	-0/+24