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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Rename to distinguish function and path composition; function composition ↵	Josh Chen	2018-08-15	1	-72/+0
\| \| \| \|	proofs, which have issues...
*	Well-formation rules are back in the methods; new theory synthesizing the ↵	Josh Chen	2018-08-14	1	-89/+69
\| \| \| \|	natural number predecessor function.
*	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 ↵	Josh Chen	2018-07-06	1	-1/+54
\| \| \| \|	be needed or useful later. Added [comp] attribute to be used by simplification met methods.
*	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 ↵	Josh Chen	2018-06-17	1	-0/+24
	well-formed contexts and guaranteed conclusion well-formedness. Product type rules now follow this scheme.