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

	Commit message (Expand)	Author	Age	Files	Lines
*	Decided on a new proper scheme for type rules using the idea of implicit well...	Josh Chen	2018-06-17	1	-23/+20
*	projections	Josh Chen	2018-06-15	1	-0/+3
*	Type rules now have \"all\" premises explicitly stated, matching the formulat...	Josh Chen	2018-06-12	1	-8/+17
*	Reorganize code	Josh Chen	2018-06-09	1	-9/+44
*	Symmetry and transitivity done.	Josh Chen	2018-06-07	1	-0/+1
*	Nondependent function arrow should bind tighter than the Pi former, but loose...	Josh Chen	2018-06-07	1	-5/+5
*	Code formatting	Josh Chen	2018-06-05	1	-0/+2
*	Proved that the inductor on Sum has the correct type.	Josh Chen	2018-06-05	1	-27/+50
*	Dependent sum done, I think.	Josh Chen	2018-06-05	1	-0/+2
*	Prod_comp should have a type constraint. This also fixes a false proof for th...	Josh Chen	2018-06-04	1	-14/+38
*	Should be final version of Prod. Theorems proving stuff about currying. Rules...	Josh Chen	2018-06-01	1	-19/+50
*	New type rules for dependent product and sum.	Josh Chen	2018-05-30	1	-9/+4
*	Fixed dependent product rules, hopefully final now.	Josh Chen	2018-05-30	1	-72/+27
*	More rigorous rules for Product type. Propositions and proofs all working, bu...	Josh Chen	2018-05-29	1	-12/+55
*	Dependent product rules done and proofs of typing properties so far work. Sta...	Josh Chen	2018-05-28	1	-37/+56
*	pre-system upgrade commit	Josh Chen	2018-05-23	1	-0/+68