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

	Commit message (Expand)	Author	Files	Lines
2018-06-27	Library organization and formatting	Josh Chen	1	-6/+7
2018-06-12	Type rules now have \"all\" premises explicitly stated, matching the formulat...	Josh Chen	1	-0/+15
2018-06-09	Reorganize code	Josh Chen	1	-248/+0
2018-06-07	Symmetry and transitivity done.	Josh Chen	1	-3/+26
2018-06-07	But also looser than Pair	Josh Chen	1	-1/+1
2018-06-07	Nondependent function arrow should bind tighter than the Pi former, but loose...	Josh Chen	1	-21/+43
2018-06-05	Code formatting	Josh Chen	1	-41/+54
2018-06-05	Proved that the inductor on Sum has the correct type.	Josh Chen	1	-17/+31
2018-06-05	Dependent sum done, I think.	Josh Chen	1	-28/+40
2018-06-04	Prod_comp should have a type constraint. This also fixes a false proof for th...	Josh Chen	1	-22/+31
2018-06-01	Should be final version of Prod. Theorems proving stuff about currying. Rules...	Josh Chen	1	-22/+15
2018-05-30	New type rules for dependent product and sum.	Josh Chen	1	-12/+29
2018-05-30	Fixed dependent product rules, hopefully final now.	Josh Chen	1	-3/+2
2018-05-29	More rigorous rules for Product type. Propositions and proofs all working, bu...	Josh Chen	1	-12/+17
2018-05-28	Dependent product rules done and proofs of typing properties so far work. Sta...	Josh Chen	1	-27/+54
2018-05-23	pre-system upgrade commit	Josh Chen	1	-35/+40
2018-05-14	Added precedences. Need to figure out how to organize metatypes.	Josh Chen	1	-13/+12
2018-05-10	Decided to go with no explicit type declarations in object-lambda expressions...	Josh Chen	1	-14/+25