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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Go back to higher-order application notation	Josh Chen	2018-09-11	1	-11/+11
\|
*	Reorganize methods	Josh Chen	2018-08-18	1	-1/+1
\|
*	Regrouping type rules	Josh Chen	2018-08-18	1	-15/+13
\|
*	Fixed mistake in Equal_elim and proof of rpathcomp_comp	Josh Chen	2018-08-18	1	-1/+1
\|
*	Prod.thy now has the correct definitional equality structure rule. ↵	Josh Chen	2018-08-16	1	-1/+1
\| \| \| \|	Definition of function composition and properties.
*	Well-formation rules are back in the methods; new theory synthesizing the ↵	Josh Chen	2018-08-14	1	-3/+7
\| \| \| \|	natural number predecessor function.
*	rcompose done	Josh Chen	2018-08-13	1	-6/+6
\|
*	Commit before testing polymorphic equality eliminator	Josh Chen	2018-08-12	1	-10/+10
\|
*	Old application syntax incompatible with Eisbach	Josh Chen	2018-08-07	1	-17/+17
\|
*	Reorganize theories	Josh Chen	2018-08-04	1	-13/+16
\|
*	Universes implemented. Type rules modified accordingly. No more automatic ↵	Josh Chen	2018-07-11	1	-8/+8
\| \| \| \|	derivation of "A:U" from "a:A".
*	Library snapshot. Methods written, everything nicely organized.	Josh Chen	2018-07-07	1	-0/+1
\|
*	Remove extra attributes for elimination rules, unneeded for now.	Josh Chen	2018-07-06	1	-2/+1
\|
*	Added attributes to type elimination rules, not sure if these will actually ↵	Josh Chen	2018-07-06	1	-0/+2
\| \| \| \|	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	-1/+1
\|
*	Fix precedence of =	Josh Chen	2018-06-30	1	-1/+1
\|
*	Equality	Josh Chen	2018-06-30	1	-54/+29
\|
*	Library organization and formatting	Josh Chen	2018-06-27	1	-1/+0
\|
*	Type rules now have \"all\" premises explicitly stated, matching the ↵	Josh Chen	2018-06-12	1	-75/+79
\| \| \| \|	formulation in the HoTT book.
*	Reorganize code	Josh Chen	2018-06-09	1	-0/+81