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

	Commit message (Collapse)	Author	Age	Files	Lines
*	(broken) update hott for Isabelle 2021-1HEAD master	stuebinm	2022-06-29	1	-6/+6
\| \| \| \| \| \| \| \| \|	this just replaces all instance of `this` with instances of `infer`. Unfortunately, it looks likes something else also broke, and I have no idea what it is (but the proof for equiv_if_equal fails). Sadly this means we can't get to univalence for now … (but rn I'm too tired to try anything else with it)
*	renamings	Josh Chen	2021-01-21	1	-30/+30
\|
*	Swapped notation for metas (now ?) and holes (now {}), other notation and ↵	Josh Chen	2021-01-18	1	-7/+7
\| \| \| \|	name changes.
*	(FEAT) Context data slots for known types and conditional type rules, as ↵	Josh Chen	2020-08-14	1	-7/+7
\| \| \| \| \| \| \| \| \| \| \| \| \|	well as a separate one for judgmental equality rules. (REF) Goal statement assumptions are now put into the new context data slots. (FEAT) `assuming` Isar keyword—like `assume` but puts assumptions into context data. (REF) Typechecking and all other tactics refactored to use type information from the context data, as opposed to looking at all facts visible in context. MINOR INCOMPATIBILITY: facts that were implicitly used in proofs now have to be annotated with [type] to make them visible throughout the context, else explicitly passed to methods via `using`, or declared with `assuming`. (REF) Fixed incompatibilities in theories.
*	(REF) Tweak attribute names in preparation for new logical introduction rule ↵	Josh Chen	2020-07-31	1	-3/+3
\| \| \| \|	behavior
*	(FEAT) Term elaboration of assumption and goal statements.	Josh Chen	2020-07-31	1	-29/+29
\| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \| \|	. 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.
*	1. Type-checking/inference now more principled, and the implementation is ↵	Josh Chen	2020-07-21	1	-8/+9
\| \| \| \|	better. 2. Changed most tactics to context tactics.
*	Non-annotated object lambda	Josh Chen	2020-07-09	1	-5/+5
\|
*	minor	Josh Chen	2020-07-08	1	-1/+1
\|
*	multiplication	Josh Chen	2020-05-31	1	-6/+72
\|
*	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
\|
*	change variable name in elim rules and fix small mistake	Josh Chen	2020-05-27	1	-7/+7
\|
*	new material	Josh Chen	2020-05-26	1	-3/+3
\|
*	more reorganizing	Josh Chen	2020-05-25	1	-1/+1
\|
*	Lists + more reorganizing	Josh Chen	2020-05-25	1	-1/+1
\|
*	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	1	-9/+10
\|
*	Brand-spanking new version using Spartan infrastructure	Josh Chen	2020-04-02	1	-0/+51