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

	Commit message (Collapse)	Author	Age	Files	Lines
*	(FEAT) SIDE_CONDS tactical has additional argument specifying how many ↵	Josh Chen	2020-08-03	2	-15/+7
\| \| \| \| \| \| \| \|	initial subgoals to skip applying the side condition solver to. (FEAT) `intro`, `intros` methods for "logical introduction rules" (as opposed to typechecking `intr` attribute), only works on conclusions with rigid type. (FEAT) CREPEAT_N bounded repetition tactical, used in `intros n` method.
*	rename some theorems	Josh Chen	2020-08-02	1	-9/+9
\|
*	(REF) Tweak attribute names in preparation for new logical introduction rule ↵	Josh Chen	2020-07-31	3	-21/+21
\| \| \| \|	behavior
*	(FEAT) Term elaboration of assumption and goal statements.	Josh Chen	2020-07-31	5	-402/+400
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	. spartan/core/goals.ML . spartan/core/elaboration.ML . spartan/core/elaborated_statement.ML (FEAT) More context tacticals and search tacticals. . spartan/core/context_tactical.ML (FEAT) Improved subgoal focus. Moves fully elaborated assumptions into the context (MINOR INCOMPATIBILITY). . spartan/core/focus.ML (FIX) Normalize facts in order to be able to resolve properly. . spartan/core/typechecking.ML (MAIN) New definitions. (MAIN) Renamed theories and theorems. (MAIN) Refactor theories to fit new features.
*	Hook elaboration into assumptions mechanism	Josh Chen	2020-07-27	2	-50/+55
\|
*	1. Bugfix: implicits now properly name schematic variables. Fixes problems ↵	Josh Chen	2020-07-21	2	-19/+22
\| \| \| \|	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.
*	1. Type-checking/inference now more principled, and the implementation is ↵	Josh Chen	2020-07-21	5	-117/+109
\| \| \| \|	better. 2. Changed most tactics to context tactics.
*	Non-annotated object lambda	Josh Chen	2020-07-09	4	-16/+16
\|
*	minor	Josh Chen	2020-07-08	2	-3/+3
\|
*	reorganize	Josh Chen	2020-06-19	1	-0/+43
\|
*	rule name	Josh Chen	2020-06-03	1	-1/+1
\|
*	reorganize and add some material	Josh Chen	2020-06-01	1	-3/+3
\|
*	multiplication	Josh Chen	2020-05-31	1	-6/+72
\|
*	transport method	Josh Chen	2020-05-31	1	-0/+2
\|
*	add and mul recurse on second argument instead of first	Josh Chen	2020-05-30	1	-20/+49
\|
*	fix name	Josh Chen	2020-05-30	1	-1/+5
\|
*	proved a few oopses + minor tweaks	Josh Chen	2020-05-29	2	-30/+23
\|
*	clean up Eckmann-Hilton and move to Identity	Josh Chen	2020-05-29	3	-209/+206
\|
*	minor	Josh Chen	2020-05-29	1	-1/+1
\|
*	change variable name in elim rules and fix small mistake	Josh Chen	2020-05-27	1	-7/+7
\|
*	minor	Josh Chen	2020-05-27	2	-8/+3
\|
*	1. Define Maybe in terms of other types. 2. Move More_Types to Spartan	Josh Chen	2020-05-27	1	-91/+0
\|
*	Eckmann-Hilton, first pass	Josh Chen	2020-05-27	2	-3/+192
\|
*	new material	Josh Chen	2020-05-26	5	-34/+58
\|
*	more reorganizing	Josh Chen	2020-05-25	4	-12/+10
\|
*	Lists + more reorganizing	Josh Chen	2020-05-25	4	-12/+14
\|
*	Reorganize theory structure. In particular, the identity type moves out from ↵	Josh Chen	2020-05-25	3	-1/+881
\| \| \| \|	under Spartan to HoTT. Spartan now only has Pi and Sigma.
*	minor	Josh Chen	2020-05-25	1	-1/+1
\|
*	some arithmetic	Josh Chen	2020-05-25	1	-17/+30
\|
*	new work on elimination tactic	Josh Chen	2020-05-24	1	-1/+1
\|
*	some tweaks and comments, in preparation for general inductive type elimination	Josh Chen	2020-05-22	1	-4/+47
\|
*	minor naming	Josh Chen	2020-04-16	1	-9/+13
\|
*	1. change var names. 2. add and mul	Josh Chen	2020-04-03	1	-8/+11
\|
*	1. Base theory. 2. Fix Nat axioms, addition.	Josh Chen	2020-04-03	2	-11/+21
\|
*	Brand-spanking new version using Spartan infrastructure	Josh Chen	2020-04-02	2	-0/+141