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

	Commit message (Collapse)	Author	Files	Lines
2019-02-28	1. Remove all type inference functionality (feature development moving to ↵	Josh Chen	1	-169/+0
	another branch). 2. Eq.thy complete.
2019-02-22	Proof of pathcomp associativity done. Some comments	Josh Chen	1	-1/+1

2019-02-11	Put typing functionality into a .thy and clean up antiquotations, which ↵	Josh Chen	1	-27/+77
	results in some reorganization of the theory import structure.
2019-02-10	restructure library	Josh Chen	1	-101/+3

2019-02-10	Explicit references in antiquotations in typing.ML. Move trace switch ↵	Josh Chen	1	-6/+3
	definition to HoTT_Base.
2019-02-10	Type information storage functionality (assume_type, assume_types keywords) ↵	Josh Chen	1	-38/+167
	done! Inference and pretty-printing for function composition done.
2019-02-05	Type inference setup begun - first use-case for function composition.	Josh Chen	1	-0/+91