| Tue, 31 Jan 2023 14:32:07 +0100 | wenzelm | removed obsolete parameter (see 7c23db6b857b); | changeset | files |
| Tue, 31 Jan 2023 12:27:00 +0100 | wenzelm | clarified Document_Editor.Session: more explicit types, more robust operations; | changeset | files |
| Mon, 30 Jan 2023 16:26:10 +0100 | wenzelm | more operations; | changeset | files |
| Mon, 30 Jan 2023 16:20:17 +0100 | wenzelm | clarified operation (without change of signature!); | changeset | files |
| Tue, 31 Jan 2023 19:07:24 +0100 | nipkow | pointless | changeset | files |
| Tue, 31 Jan 2023 14:05:16 +0000 | paulson | Lots more new material thanks to Manuel Eberl | changeset | files |
| Mon, 30 Jan 2023 15:24:25 +0000 | paulson | merged | changeset | files |