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

	Commit message (Collapse)	Author	Age	Files	Lines
*	begin work on pre-proof elaboration	Josh Chen	2020-07-22	2	-19/+218
\|
*	minor	Josh Chen	2020-07-21	1	-1/+1
\|
*	1. Bugfix: implicits now properly name schematic variables. Fixes problems ↵	Josh Chen	2020-07-21	4	-35/+45
\| \| \| \|	caused by variable name clashes. 2. reduce method now more principled: restricts to repeating on first subgoal. 3. An example declarative proof in Equivalence.thy.
*	Merge pull request #8 from jaycech3n/dev	Josh Chen	2020-07-21	16	-431/+603
\|\ \| \| \| \|	Merge big diff on dev
\| *	1. Type-checking/inference now more principled, and the implementation is ↵	Josh Chen	2020-07-21	16	-622/+394
\| \| \| \| \| \| \| \|	better. 2. Changed most tactics to context tactics.
\| *	Checkpoint. THIS BUILD WILL FAIL	Josh Chen	2020-07-16	6	-51/+451
\| \|
* \|	link	Josh Chen	2020-07-17	1	-1/+1
\| \|
* \|	add build status	Josh Chen	2020-07-17	1	-1/+1
\| \|
* \|	rename action	Josh Chen	2020-07-17	1	-1/+1
\| \|
* \|	Merge pull request #7 from jaycech3n/ci-action	Josh Chen	2020-07-17	3	-8/+14
\|\ \ \| \| \| \| \| \|	Ci action
\| * \|	looks like descriptions not allowed in workflow job yaml	Josh Chen	2020-07-17	1	-1/+0
\| \| \|
\| * \|	final test push	Josh Chen	2020-07-17	2	-0/+2
\| \| \|
\| * \|	fix path	Josh Chen	2020-07-17	1	-2/+3
\| \| \|
\| * \|	test	Josh Chen	2020-07-17	3	-8/+11
\| \| \|
\| * \|	check home var	Josh Chen	2020-07-17	1	-1/+1
\| \| \|
\| * \|	change HOME env var, more testing...	Josh Chen	2020-07-17	1	-1/+2
\|/ /
* \|	more test	Josh Chen	2020-07-17	1	-0/+1
\| \|
* \|	more testing	Josh Chen	2020-07-17	3	-14/+9
\| \|
* \|	probe directories	Josh Chen	2020-07-16	1	-1/+1
\| \|
* \|	test	Josh Chen	2020-07-16	1	-1/+2
\| \|
* \|	try try again	Josh Chen	2020-07-16	3	-7/+8
\| \|
* \|	try again	Josh Chen	2020-07-16	1	-6/+6
\| \|
* \|	I think I figured out the problem	Josh Chen	2020-07-16	1	-2/+1
\| \|
* \|	try ADD instead of RUN curl	Josh Chen	2020-07-16	1	-2/+1
\| \|
* \|	will this parse now?	Josh Chen	2020-07-16	1	-1/+2
\| \|
* \|	fix	Josh Chen	2020-07-16	1	-1/+1
\| \|
* \|	download Isabelle from TUM archives	Josh Chen	2020-07-16	1	-2/+3
\| \|
* \|	fix action path	Josh Chen	2020-07-16	1	-1/+1
\| \|
* \|	set up CI	Josh Chen	2020-07-16	3	-0/+53
\|/
*	update readme	Josh Chen	2020-07-16	1	-2/+2
\|
*	Defined annotated terms to be used in future typechecking improvements	Josh Chen	2020-07-11	1	-4/+7
\|
*	fix file location reference in license	Josh Chen	2020-07-11	1	-2/+2
\|
*	rename file	Josh Chen	2020-07-11	1	-2/+26
\|
*	Non-annotated object lambda	Josh Chen	2020-07-09	8	-56/+78
\|
*	caveat	Josh Chen	2020-07-09	1	-0/+2
\|
*	1. Initial `Definition` keyword. 2. ifelse.	Josh Chen	2020-07-08	5	-28/+76
\|
*	minor	Josh Chen	2020-07-08	2	-3/+3
\|
*	reorganize	Josh Chen	2020-06-19	29	-2005/+105
\|
*	fix ROOT	Josh Chen	2020-06-15	1	-1/+1
\|
*	remove old folder	Josh Chen	2020-06-15	3	-372/+0
\|
*	Merge branch 'dev'	Josh Chen	2020-06-15	17	-18/+2344
\|\
\| *	rename folders	Josh Chen	2020-06-15	15	-0/+2339
\| \|
\| *	some documentation	Josh Chen	2020-06-04	2	-15/+2
\| \|
* \|	Merge branch 'dev'	Josh Chen	2020-06-03	5	-6/+33
\|\\|
\| *	rule name	Josh Chen	2020-06-03	1	-1/+1
\| \|
\| *	1. Type information context data	Josh Chen	2020-06-03	4	-5/+32
\| \| \| \| \| \| \| \| \| \|	2. Small reformulations of rules 3. Bool
* \|	update	Josh Chen	2020-06-01	1	-4/+4
\|/
*	update	Josh Chen	2020-06-01	1	-0/+1
\|
*	update	Josh Chen	2020-06-01	1	-6/+7
\|
*	reorganize and add some material	Josh Chen	2020-06-01	2	-44/+62
\|