Isabelle-HoTT/spartan/lib, branch master trying to make Isabelle/HoTT work with Isabelle 2021-1 https://stuebinm.eu/git/Isabelle-HoTT/atom/spartan/lib?h=master 2021-01-31T02:54:51Z rename things + some small changes 2021-01-31T02:54:51Z Josh Chen 2021-01-31T02:54:51Z urn:sha1:2feb56660700af107abb5a28a7120052ac405518 renamings 2021-01-21T00:52:13Z Josh Chen 2021-01-21T00:52:13Z urn:sha1:aff3d43d9865e7b8d082f0c239d2c73eee1fb291 Swapped notation for metas (now ?) and holes (now {}), other notation and name changes. 2021-01-18T23:49:13Z Josh Chen 2021-01-18T23:49:13Z urn:sha1:f46df86db9308dde29e0e5f97f54546ea1dc34bf (FEAT) Context data slots for known types and conditional type rules, as well as a separate one for judgmental equality rules. 2020-08-14T09:07:17Z Josh Chen 2020-08-14T09:07:17Z urn:sha1:bd2efacaf67ae84c41377e7af38dacc5aa64f405 (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 behavior 2020-07-31T16:10:10Z Josh Chen 2020-07-31T16:10:10Z urn:sha1:77aa10763429d2ded040071fbf7bee331dd52f5e (FEAT) Term elaboration of assumption and goal statements. 2020-07-31T12:56:24Z Josh Chen 2020-07-31T12:56:24Z urn:sha1:ff5454812f9e2720bd90c3a5437505644f63b487 . 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 better. 2. Changed most tactics to context tactics. 2020-07-21T00:09:44Z Josh Chen 2020-07-21T00:09:44Z urn:sha1:12eed8685674b7d5ff7bc45a44a061e01f99ce5f Non-annotated object lambda 2020-07-09T11:35:39Z Josh Chen 2020-07-09T11:35:39Z urn:sha1:831f33468f227c0dc96bd31380236f2c77e70c52 1. Initial `Definition` keyword. 2. ifelse. 2020-07-08T13:55:48Z Josh Chen 2020-07-08T13:55:48Z urn:sha1:07c51b1801bd701bef61cedd571a944d9bd37e8b rename folders 2020-06-15T09:52:19Z Josh Chen 2020-06-15T09:52:19Z urn:sha1:69bf0744a5ce3ba144f59564ebf74d7d2f56b748