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

	Commit message (Collapse)	Author	Age	Files	Lines
*	Not sure what advantage is provided by having eta-expanded forms in the ↵	Josh Chen	2018-09-19	1	-3/+3
\| \| \| \|	rules. Removing for now.
*	Overhaul of the theory presentations. New methods in HoTT_Methods.thy for ↵	Josh Chen	2018-09-18	1	-0/+1
\| \| \| \|	handling universes. Commit for release 0.1.0!
*	Reorganizing theories	Josh Chen	2018-09-17	1	-33/+27
\|
*	Reorganized HoTT_Base, updated theories	Josh Chen	2018-09-16	1	-18/+18
\|\
\| *	Go back to higher-order application notation	Josh Chen	2018-09-11	1	-14/+14
\|/
*	Reorganize methods	Josh Chen	2018-08-18	1	-1/+1
\|
*	Regrouping type rules	Josh Chen	2018-08-18	1	-10/+9
\|
*	Cleanups	Josh Chen	2018-08-17	1	-4/+4
\|
*	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	-0/+5
\| \| \| \|	natural number predecessor function.
*	Equality inverse and composition done. Cleaned up methods and method example ↵	Josh Chen	2018-08-14	1	-1/+1
\| \| \| \|	theory.
*	rcompose done	Josh Chen	2018-08-13	1	-0/+1
\|
*	Old application syntax incompatible with Eisbach	Josh Chen	2018-08-07	1	-15/+15
\|
*	Partway through changing function application syntax style.	Josh Chen	2018-08-06	1	-0/+49