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

	Commit message (Expand)	Author	Age	Files	Lines
*	Prod.thy now has the correct definitional equality structure rule. Definition...	Josh Chen	2018-08-16	1	-1/+1
*	Rename to distinguish function and path composition; function composition pro...	Josh Chen	2018-08-15	1	-20/+20
*	Basic compute method	Josh Chen	2018-08-15	1	-6/+6
*	Tweak proof methods, some type rules; add HoTT Book examples	Josh Chen	2018-08-15	1	-29/+29
*	Function composition, rename path composition to differentiate the two.	Josh Chen	2018-08-15	1	-20/+20
*	Equality inverse and composition done. Cleaned up methods and method example ...	Josh Chen	2018-08-14	1	-40/+152
*	rcompose done	Josh Chen	2018-08-13	1	-18/+60
*	Commit before testing polymorphic equality eliminator	Josh Chen	2018-08-12	1	-13/+16
*	Universes implemented. Type rules modified accordingly. No more automatic der...	Josh Chen	2018-07-11	1	-5/+8
*	Pre-universe implementation commit	Josh Chen	2018-07-09	1	-15/+10
*	Library snapshot. Methods written, everything nicely organized.	Josh Chen	2018-07-07	1	-14/+8
*	Added attributes to type elimination rules, not sure if these will actually b...	Josh Chen	2018-07-06	1	-21/+0
*	Refactor HoTT_Methods.thy, proved more stuff with new methods.	Josh Chen	2018-07-03	1	-25/+25
*	Rewrote methods: wellformed now two lines, uses named theorems. New, more pow...	Josh Chen	2018-07-03	1	-30/+18
*	Proving path composition. Need to set up the Simplifier to simplify applicati...	Josh Chen	2018-06-30	1	-10/+28
*	Equality	Josh Chen	2018-06-30	1	-0/+90