| 30e48cd | Josh Chen | 10 April 2021, 21:06:59 UTC | update Isabelle2020 URL in Dockerfile | 10 April 2021, 21:06:59 UTC |
| 2570ac5 | Josh Chen | 01 February 2021, 13:03:19 UTC | update readme | 01 February 2021, 13:03:19 UTC |
| 2feb566 | Josh Chen | 31 January 2021, 02:54:51 UTC | rename things + some small changes | 31 January 2021, 02:54:51 UTC |
| aff3d43 | Josh Chen | 21 January 2021, 00:52:13 UTC | renamings | 21 January 2021, 00:52:13 UTC |
| 6d8fa47 | Josh Chen | 19 January 2021, 02:44:03 UTC | Forgot to update ROOT | 19 January 2021, 02:44:03 UTC |
| 549f1d4 | Josh Chen | 19 January 2021, 02:18:44 UTC | Bugfix: no longer repeatedly add duplicate rules to simpset | 19 January 2021, 02:18:44 UTC |
| f46df86 | Josh Chen | 18 January 2021, 23:49:13 UTC | Swapped notation for metas (now ?) and holes (now {}), other notation and name changes. | 18 January 2021, 23:49:13 UTC |
| 3922e24 | Josh Chen | 23 September 2020, 15:03:42 UTC | Basic experiments adding reduction to the type checker | 23 September 2020, 15:03:42 UTC |
| 77df99b | Josh Chen | 14 August 2020, 17:55:38 UTC | minor | 14 August 2020, 17:55:38 UTC |
| d172f9d | Josh Chen | 14 August 2020, 09:21:59 UTC | reorganize | 14 August 2020, 09:21:59 UTC |
| 7a53528 | Josh Chen | 14 August 2020, 09:11:34 UTC | update license file list | 14 August 2020, 09:11:34 UTC |
| bd2efac | Josh Chen | 14 August 2020, 09:07:17 UTC | (FEAT) Context data slots for known types and conditional type rules, as 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. | 14 August 2020, 09:07:17 UTC |
| 8f4ff41 | Josh Chen | 09 August 2020, 16:34:58 UTC | (FEAT) Clean up typechecking/elaboration tactic: known_ctac should *solve* goals; resolving with conditional typing judgments (e.g. type family assumptions) is part of check_infer_step | 09 August 2020, 16:34:58 UTC |
| c530305 | Josh Chen | 05 August 2020, 13:21:43 UTC | 1. fix intros method. 2. Couple extra lemmas; good small test cases for normalization in typechecking/elaboration. | 05 August 2020, 13:21:43 UTC |
| 710f314 | Josh Chen | 03 August 2020, 11:34:53 UTC | (FEAT) SIDE_CONDS tactical has additional argument specifying how many 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. | 03 August 2020, 11:34:53 UTC |
| 70fd3f7 | Josh Chen | 02 August 2020, 14:44:47 UTC | rename some theorems | 02 August 2020, 14:44:47 UTC |
| 77aa107 | Josh Chen | 31 July 2020, 16:10:10 UTC | (REF) Tweak attribute names in preparation for new logical introduction rule behavior | 31 July 2020, 16:10:10 UTC |
| ff54548 | Josh Chen | 31 July 2020, 12:56:24 UTC | (FEAT) Term elaboration of assumption and goal statements. . 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. | 31 July 2020, 12:56:24 UTC |
| 2b0e14b | Josh Chen | 28 July 2020, 12:24:22 UTC | small improvement | 28 July 2020, 12:24:22 UTC |
| 6b27aa5 | Josh Chen | 28 July 2020, 12:10:34 UTC | New `assuming` proof command for elaborated assumptions | 28 July 2020, 12:10:34 UTC |
| 223a253 | Josh Chen | 27 July 2020, 12:31:35 UTC | Merge branch 'dev' | 27 July 2020, 12:31:35 UTC |
| 2a78ddc | Josh Chen | 27 July 2020, 12:31:09 UTC | update .gitignore | 27 July 2020, 12:31:09 UTC |
| 0f84aa0 | Josh Chen | 27 July 2020, 12:29:48 UTC | Hook elaboration into assumptions mechanism | 27 July 2020, 12:29:48 UTC |
| f20d91f | Josh Chen | 23 July 2020, 11:00:04 UTC | minor | 23 July 2020, 11:00:04 UTC |
| 184b1d4 | Josh Chen | 22 July 2020, 13:48:33 UTC | remove theory | 22 July 2020, 13:48:33 UTC |
| 4be339f | Josh Chen | 22 July 2020, 13:30:27 UTC | begin work on pre-proof elaboration | 22 July 2020, 13:30:27 UTC |
| 6464ab5 | Josh Chen | 21 July 2020, 17:31:31 UTC | minor | 21 July 2020, 17:31:31 UTC |
| 3067216 | Josh Chen | 21 July 2020, 14:28:05 UTC | 1. Bugfix: implicits now properly name schematic variables. Fixes problems 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. | 21 July 2020, 14:28:05 UTC |
| dfd241b | Josh Chen | 21 July 2020, 00:16:14 UTC | Merge pull request #8 from jaycech3n/dev Merge big diff on dev | 21 July 2020, 00:16:14 UTC |
| 12eed86 | Josh Chen | 21 July 2020, 00:09:44 UTC | 1. Type-checking/inference now more principled, and the implementation is better. 2. Changed most tactics to context tactics. | 21 July 2020, 00:09:44 UTC |
| 6aaf4d5 | Josh Chen | 17 July 2020, 11:48:30 UTC | link | 17 July 2020, 11:48:30 UTC |
| 1130633 | Josh Chen | 17 July 2020, 09:30:34 UTC | add build status | 17 July 2020, 09:30:34 UTC |
| de4d802 | Josh Chen | 17 July 2020, 09:27:42 UTC | rename action | 17 July 2020, 09:27:42 UTC |
| b7439e6 | Josh Chen | 17 July 2020, 09:15:26 UTC | Merge pull request #7 from jaycech3n/ci-action Ci action | 17 July 2020, 09:15:26 UTC |
| 00463d7 | Josh Chen | 17 July 2020, 09:12:00 UTC | looks like descriptions not allowed in workflow job yaml | 17 July 2020, 09:12:00 UTC |
| 9eb4aeb | Josh Chen | 17 July 2020, 09:11:13 UTC | final test push | 17 July 2020, 09:11:13 UTC |
| f510ca7 | Josh Chen | 17 July 2020, 09:06:19 UTC | fix path | 17 July 2020, 09:06:19 UTC |
| 877b951 | Josh Chen | 17 July 2020, 09:03:22 UTC | test | 17 July 2020, 09:03:22 UTC |
| 66b180a | Josh Chen | 17 July 2020, 08:51:26 UTC | check home var | 17 July 2020, 08:51:26 UTC |
| 6e54cf5 | Josh Chen | 17 July 2020, 08:47:20 UTC | change HOME env var, more testing... | 17 July 2020, 08:47:20 UTC |
| 1ff98c9 | Josh Chen | 17 July 2020, 08:41:19 UTC | more test | 17 July 2020, 08:41:19 UTC |
| 31dca57 | Josh Chen | 17 July 2020, 08:35:07 UTC | more testing | 17 July 2020, 08:35:07 UTC |
| e75a2a2 | Josh Chen | 16 July 2020, 21:31:04 UTC | probe directories | 16 July 2020, 21:31:04 UTC |
| 6f2dc47 | Josh Chen | 16 July 2020, 21:28:28 UTC | test | 16 July 2020, 21:28:28 UTC |
| 61f2b77 | Josh Chen | 16 July 2020, 21:24:34 UTC | try try again | 16 July 2020, 21:24:34 UTC |
| 64a41c3 | Josh Chen | 16 July 2020, 17:53:11 UTC | try again | 16 July 2020, 17:53:11 UTC |
| 1f98940 | Josh Chen | 16 July 2020, 17:33:51 UTC | I think I figured out the problem | 16 July 2020, 17:33:51 UTC |
| f2614cb | Josh Chen | 16 July 2020, 17:31:55 UTC | try ADD instead of RUN curl | 16 July 2020, 17:31:55 UTC |
| a31c2a9 | Josh Chen | 16 July 2020, 17:25:46 UTC | will this parse now? | 16 July 2020, 17:25:46 UTC |
| ddb5325 | Josh Chen | 16 July 2020, 17:22:32 UTC | fix | 16 July 2020, 17:22:32 UTC |
| 402a802 | Josh Chen | 16 July 2020, 17:19:03 UTC | download Isabelle from TUM archives | 16 July 2020, 17:19:03 UTC |
| d81a1db | Josh Chen | 16 July 2020, 16:59:34 UTC | fix action path | 16 July 2020, 16:59:34 UTC |
| f822581 | Josh Chen | 16 July 2020, 16:57:13 UTC | set up CI | 16 July 2020, 16:57:13 UTC |
| 3bcaf5d | Josh Chen | 16 July 2020, 14:46:09 UTC | Checkpoint. THIS BUILD WILL FAIL | 16 July 2020, 14:46:09 UTC |
| 2a2fa1e | Josh Chen | 16 July 2020, 14:20:15 UTC | update readme | 16 July 2020, 14:20:15 UTC |
| 79659cb | Josh Chen | 11 July 2020, 13:13:20 UTC | Defined annotated terms to be used in future typechecking improvements | 11 July 2020, 13:13:20 UTC |
| 7d59cf1 | Josh Chen | 11 July 2020, 13:11:37 UTC | fix file location reference in license | 11 July 2020, 13:11:44 UTC |
| 8612748 | Josh Chen | 11 July 2020, 13:10:42 UTC | rename file | 11 July 2020, 13:10:42 UTC |
| 831f334 | Josh Chen | 09 July 2020, 11:35:39 UTC | Non-annotated object lambda | 09 July 2020, 11:35:39 UTC |
| fc9ba21 | Josh Chen | 09 July 2020, 10:58:13 UTC | caveat | 09 July 2020, 10:58:13 UTC |
| 07c51b1 | Josh Chen | 08 July 2020, 13:55:48 UTC | 1. Initial `Definition` keyword. 2. ifelse. | 08 July 2020, 13:55:48 UTC |
| f0fab6e | Josh Chen | 08 July 2020, 13:54:04 UTC | minor | 08 July 2020, 13:54:04 UTC |
| 4f147cb | Josh Chen | 19 June 2020, 10:41:54 UTC | reorganize | 19 June 2020, 10:41:54 UTC |
| 8885f9c | Josh Chen | 15 June 2020, 09:58:30 UTC | fix ROOT | 15 June 2020, 09:58:30 UTC |
| 28e91f9 | Josh Chen | 15 June 2020, 09:56:28 UTC | remove old folder | 15 June 2020, 09:56:28 UTC |
| e42b7b3 | Josh Chen | 15 June 2020, 09:53:44 UTC | Merge branch 'dev' | 15 June 2020, 09:53:44 UTC |
| 69bf074 | Josh Chen | 15 June 2020, 09:52:19 UTC | rename folders | 15 June 2020, 09:52:19 UTC |
| 8d6d633 | Josh Chen | 04 June 2020, 12:27:41 UTC | some documentation | 04 June 2020, 12:27:41 UTC |
| 9050b74 | Josh Chen | 03 June 2020, 11:10:35 UTC | Merge branch 'dev' | 03 June 2020, 11:10:35 UTC |
| 515c142 | Josh Chen | 03 June 2020, 11:09:45 UTC | rule name | 03 June 2020, 11:09:45 UTC |
| e513fc2 | Josh Chen | 03 June 2020, 11:09:30 UTC | 1. Type information context data 2. Small reformulations of rules 3. Bool | 03 June 2020, 11:09:30 UTC |
| ccc26cf | Josh Chen | 01 June 2020, 15:33:40 UTC | update | 01 June 2020, 15:33:47 UTC |
| 8c0205a | Josh Chen | 01 June 2020, 15:26:39 UTC | update | 01 June 2020, 15:26:39 UTC |
| cf5136f | Josh Chen | 01 June 2020, 15:22:09 UTC | update | 01 June 2020, 15:22:09 UTC |
| 29112d6 | Josh Chen | 01 June 2020, 15:19:27 UTC | reorganize and add some material | 01 June 2020, 15:19:27 UTC |
| 0834e99 | Josh Chen | 01 June 2020, 15:18:39 UTC | readme | 01 June 2020, 15:18:39 UTC |
| dc3800f | Josh Chen | 31 May 2020, 11:14:35 UTC | more list | 31 May 2020, 11:14:35 UTC |
| c3606c3 | Josh Chen | 30 May 2020, 23:13:42 UTC | multiplication | 30 May 2020, 23:13:42 UTC |
| 4faad4f | Josh Chen | 30 May 2020, 23:13:34 UTC | transport method | 30 May 2020, 23:13:34 UTC |
| 1263127 | Josh Chen | 30 May 2020, 16:29:46 UTC | add and mul recurse on second argument instead of first | 30 May 2020, 16:29:46 UTC |
| 68bbcdc | Josh Chen | 30 May 2020, 16:29:11 UTC | inhabitation coercion should be syntax, not logical constant! | 30 May 2020, 16:29:11 UTC |
| 2e807b7 | Josh Chen | 30 May 2020, 12:38:12 UTC | fix name | 30 May 2020, 12:38:12 UTC |
| 9ed05b8 | Josh Chen | 29 May 2020, 17:59:22 UTC | proved a few oopses + minor tweaks | 29 May 2020, 17:59:22 UTC |
| 02cfe2a | Josh Chen | 29 May 2020, 17:58:29 UTC | fix Pi congruence rule | 29 May 2020, 17:58:29 UTC |
| 484988b | Josh Chen | 29 May 2020, 12:28:17 UTC | todo list | 29 May 2020, 12:28:17 UTC |
| 2f4e9b9 | Josh Chen | 29 May 2020, 08:37:46 UTC | clean up Eckmann-Hilton and move to Identity | 29 May 2020, 08:37:46 UTC |
| 41da54e | Josh Chen | 29 May 2020, 08:20:36 UTC | minor | 29 May 2020, 08:20:36 UTC |
| 417af1a | Josh Chen | 28 May 2020, 14:00:42 UTC | bit more material | 28 May 2020, 14:00:42 UTC |
| 17b9392 | Josh Chen | 28 May 2020, 14:00:31 UTC | notation | 28 May 2020, 14:00:31 UTC |
| 1ccd936 | Josh Chen | 28 May 2020, 12:08:26 UTC | more List and Maybe | 28 May 2020, 12:08:26 UTC |
| 6ff59c8 | Josh Chen | 28 May 2020, 12:07:52 UTC | case distinction | 28 May 2020, 12:07:52 UTC |
| a9606c9 | Josh Chen | 28 May 2020, 10:54:40 UTC | reorganize folder structure | 28 May 2020, 10:54:40 UTC |
| f12983b | Josh Chen | 27 May 2020, 20:16:42 UTC | change variable name in elim rules and fix small mistake | 27 May 2020, 20:16:42 UTC |
| ed41980 | Josh Chen | 27 May 2020, 19:31:57 UTC | minor | 27 May 2020, 19:31:57 UTC |
| 62c1c8f | Josh Chen | 27 May 2020, 19:31:35 UTC | 1. Define Maybe in terms of other types. 2. Move More_Types to Spartan | 27 May 2020, 19:31:35 UTC |
| ec7dcd5 | Josh Chen | 27 May 2020, 19:30:21 UTC | move More_Types to Spartan | 27 May 2020, 19:30:21 UTC |
| fd8ae0b | Josh Chen | 26 May 2020, 23:18:46 UTC | Eckmann-Hilton, first pass | 26 May 2020, 23:18:46 UTC |
| b0ba102 | Josh Chen | 26 May 2020, 14:50:35 UTC | new material | 26 May 2020, 14:50:35 UTC |
| 028f43a | Josh Chen | 26 May 2020, 14:50:13 UTC | 1. New congruence declarations for calculational reasoning. 2. Remove old elimination tactic. | 26 May 2020, 14:50:13 UTC |
| 8ba8357 | Josh Chen | 26 May 2020, 14:39:35 UTC | Maybe and more List | 26 May 2020, 14:39:35 UTC |
