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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Moved function composition lemmas into Prod.thy	Josh Chen	2018-09-17	1	-57/+0
\|
*	Some final touchups before release 0.1 for the MS thesis	Josh Chen	2018-09-12	1	-1/+1
\|
*	Add the univalence axiom	Josh Chen	2018-09-11	1	-0/+5
\|
*	Go back to higher-order application notation	Josh Chen	2018-09-11	1	-6/+6
\|
*	Reorganize methods	Josh Chen	2018-08-18	1	-6/+6
\|
*	Regrouping type rules	Josh Chen	2018-08-18	1	-2/+1
\|
*	Misc formatting	Josh Chen	2018-08-18	1	-1/+0
\|
*	Properties of function composition	Josh Chen	2018-08-17	1	-24/+5
\|
*	Partway through updating proofs after the change of the function composition ↵	Josh Chen	2018-08-17	1	-46/+11
\| \| \| \|	definition
*	Prod.thy now has the correct definitional equality structure rule. ↵	Josh Chen	2018-08-16	1	-23/+77
\| \| \| \|	Definition of function composition and properties.
*	Rename to distinguish function and path composition; function composition ↵	Josh Chen	2018-08-15	1	-0/+54
	proofs, which have issues...