- Make the search by pattern more flexible. Search by pattern version 2 (#237)
- Bug fix: Extra spaces around description when opening proof in editor. #245
- Add "Referenced by" filter to the Explorer tab.
- Sort assertions on the Explorer tab. #235
- Bug fix: Crash when adding statements with "use". #239
- Bug fix: DV conditions can oscillate and prevent editing. #241
- Add "Depends on" filter to the Explorer tab. This filter allows to quickly find all assertions which depend (directly and transitively) on the given assertion.
- Support label mode in comments (labels and URLs are clickable in comments).
- Partially support math mode in comments (additional styling is applied to symbols in math mode in comments, but typesetting is not supported).
- Usability improvement: add some styling to tabs to make it easier to switch between tabs.
- Multiple editor tabs. #153
- Bug fix: Search by description produces misleading results. #215
- Updates in the macros API.
- Updates in the "set.mm example macros" collection of macros.
- Improve usability of the assertion search dialog in the editor.
- Update the "inline proof" feature: instead of inlining the theorem for a single step, it is now possible to inline multiple theorems (and all steps using those theorems) at once.
- A new feature "Reorder steps". It automatically reorders steps taking into account dependencies between them.
- Possibility to reorder bookmarked steps when only bookmarked steps are displayed.
- Slight changes in the formatting of the completed proof.
- Enable automatic substitution search to minimize presses of the "Find Substitution" button.
- Add "Show unproved only" and "Expand all sources" buttons to the Proof Tree dialog.
- Bug fix: scrolling position changes "randomly" when switching between tabs.
- Allow selecting multiple steps in the editor by holding the Shift key.
- Add the option to include all hypotheses (even unused ones) in the compressed proof.
- Add the "Apply a substitution to all steps" button to the fragment selection actions.
- Add an additional pagination UI element at the bottom of the Explorer page.
- Make it possible to change default parameter values for the bottom-up prover.
- Fix a bug in "Find substitution by unification".
- Add a "Restore default settings" button to the Settings tab.
- Bug fix: Use spaces instead of commas to separate variables in the disjoints section of the editor. #199
- Extend the pattern search functionality: match assertions and hypotheses simultaneously; match assertion and hypotheses separately; adjacent symbols (#57); exact match.
- Allow opening a new Explorer tab with empty search filters.
- Add possibility to bookmark steps in the Editor. This allows to show only bookmarked steps.
- Add pagination in the Editor to simplify work with long proofs. Number of steps per page is configurable in the "View options" menu.
- Add a new transform "Extract: X ⇒ ( ph -> X )" which extracts a part of a step in a deduction proof.
- Add possibility to "Delete unrelated steps and hypotheses" in the Editor.
- Allow specifying steps for the "Allowed statements: first level" option of the bottom-up prover by selecting steps in the editor before invoking the bottom-up prover dialog.
- Implement the "Inline proof" in the editor.
- Make it possible to move all selected steps to the top or bottom in the Editor.
- Make it possible to add assertions from the Explorer tab to the Editor. This is an equivalent of using the Search button in the Editor, but more handy in some cases.
- Add filtering by description in the Explorer. #178
- Bug fix: An assertion tab crashes if the assertion proof contains errors. #184
- Bug fix: Renumber fails if the goal label is a number. #207
- Implement pagination in the Proof Explorer.
- Add "About this application" button on the Settings tab. #72
- In the bottom-up prover dialog, add possibility to set "Allowed statements: other levels" equal to "Allowed statements: first level".
- Change the default value of "Allowed statements: first level" to None in the bottom-up prover dialog.
- Changes in the API of the Fragment Transform feature.
- Make it possible to run a macro from the UI.
- Migrate to ReScript 11. No functional changes.
- Add a new validation in the Editor: "Any statement must begin with a constant".
- Add more info to the Merge dialog to understand easier what statement to use #188
- Implement the feature of Macros in the experimental mode (this allows to automate certain actions in Metamath-lamp using custom JavaScript code). In this version it is not possible to run a macro from the UI.
- Support variables in the pattern search (#13)
- Implement the "Delete unrelated steps" feature in the Editor.
- Implement the "Rename hypotheses" feature in the Editor.
- Implement the "Auto unify all" feature in the Editor.
- Usability improvement: Add empty space at the bottom of the editor for longer proofs.
- Usability improvement: Allow sorting by "Number of new steps" in the Bottom-up prover dialog.
- Set the default value of "Allow new variables" in the bottom-up prover to False #180
- Bug fix: Unify hangs for certain statements/theorems #175
- Always sort variables in disjoints according to the specified order #172
- Allow opening multiple Explorer tabs by clicking the "search" button on a selected fragment.
- Change the order in which assertions are selected by the prover #163
- Bug fix: Bottom-up prover adds unnecessary disjoints #166
- Usability improvement: Make it possible to manually add disjoints on mobile #164
- Implement "Fragment Transformers" (#121)
- Implement rules how to work with
discouraged/deprecated/transitively deprecatedassertions #31 #111 - Add "Duplicate up" button in the Editor #154
- Usability improvement: When substituting, always use the most recent selections #155
- In the Explorer allow selection of final type #111
- Preload existing proofs into the editor #8
- For goal labels, apply same strict label validation rules as for hypotheses #81
- Make it more obvious how to get a completed proof #11
- Allow merging multiple statements with one merge button click #149
- Automatic merge of duplicated statements (#47)
- Usability improvement: Replacement fields should use selections consistently in the Substitution dialog #82
- Full unification in the Substitution dialog #147
- Add a "Reset editor content" menu item in the Editor #21
- Automate creating of labels for hypotheses (#32)
- Make it possible to switch on/off parentheses autocomplete #64
- Usability improvement: Open proof explorer by clicking refs in justifications #99
- Usability improvement: Add delete (trash can) when editing Description, Variables, and Disjoints #123
- Usability improvement: Allow shrinking to a single symbol in fragment selector #112
- UI improvement: In visualizations, don't repeat if conclusion is all constants #115
- Bug fix: Alt+click doesn't edit label and step type when "long click" is enabled #138
- The undo/redo feature in the editor #133