-
Notifications
You must be signed in to change notification settings - Fork 5
Closed
Labels
Description
Current way of merging of duplicated statements involves some manual work. In many cases it could be automated. Currently the process of merging is as follows:
- Select the statement this error message "This statement is the same as the previous one - 'label'" appeared for by clicking the checkbox left to the statement. This must be the statement right above the error message. And make sure this is the only statement selected.
- Click "Merge two similar statements" button. This button looks like two lines merging into a single line (like Y).
- A dialog should appear where you will have possibility to select what statement you want to continue using. (you selected one statement, metamath-lamp finds another duplicated statement automatically)
This way one of the duplicated statements will be removed automatically and metamath-lamp will update all the justifications which used the removed statement so they will use the statement you chose to continue using.