<\body> When writing documents in collaboration with other authors, it frequently arises that one wants to go through changes made by the other authors, and either accept, discard or further correct them. After enabling the versioning tool through , aspecial menu appears in the main menu bar, which makes this process automatic. Let us describe in more detail how this tool works. For the moment, automatic version control systems such as are not yet supported. In the future, we intend to include support for such systems and the operation of merging two different new versions. Assume that we have two versions and of the same document. In order to see the changes, first load the newest version , then click on and select the oldest version . The buffer will still be named , and the changes between both versions will be indicated by special markup. If there are any changes, then the cursor will be positioned at the first difference. It is possible to go through all the differences between the old and new versions either from the items in the submenu , or using the keyboard shortcuts and . One may also use the more general structured navigation shortcuts , , and . Differences between the two versions can be displayed in three ways: by showing only the old version, only the new version, or both versions simultaneously. In all cases, the old version is displayed in dark red and the new version in dark green. The visualization style can be specified individually for each individual change, via or the keyboard shortcuts (old version), (new version) and (both versions). One may also cycle through the different style using the structured variant key . If you selected some text, then the above actions will apply to the whole selection. The visualization style may also be specified globally, using , and . It often occurs that we want to go through the changes between two versions and progressively retain either one or the other version for each individual difference. Assuming that the cursor is inside a given difference, this can be done from entries in the submenu . Alternatively, one may use the shortcuts , and to retain the old, new and currently displayed version, respectively. If both versions are displayed, then retains the new version. After retaining one of the versions, we automatically jump to the next difference, which can then be processed. If you selected some text, then any of the above action will retain the appropriate version for each of the differences in the selection. It is also possible to globally select the old, new or current version using , , . A convenient alternative way to process all differences is to use and to go through the differences, use and to select the preferred version, and then click on as soon as all differences have been processed. The entries in the submenu allow you to control the grain with which differences between versions are computed. By default, we use the finest grain . It is also possible to compute differences on a paragraph-based level, using . In that case, the entire paragraphs in which a change occurs will be highlighted. The roughest grain will highlight the entire text, if a change occurs within it. The grain is used when comparing two documents using , but it is also possible to recompare the differences in a selected portion of text using . The latter possibility is especially useful after a change the grain. Similarly, the cursor is inside a difference, then you may recompare the two versions . This may be useful, if you made some changes to one of the versions. For instance, assume that the old version contained a theorem and that we changed it into a lemma in the new version and also modified part of its inside text. When visualizing the changes, the whole theorem will be highlighted, since there is no appropriate markup to indicate that we just changed from atheorem to a lemma. Nevertheless, if we want to compare the inside texts, we may turn the old theorem into a lemma and then click on . <\initial> <\collection>