| Mon, 12 Apr 2021 15:00:03 +0200 | wenzelm | clarified message output: flush already happens in write_message_yxml (see Isabelle/22b5ecb53dd9); | changeset | files |
| Mon, 12 Apr 2021 14:14:47 +0200 | wenzelm | tuned; | changeset | files |
| Mon, 12 Apr 2021 12:32:09 +0200 | wenzelm | clarified cache; | changeset | files |
| Mon, 12 Apr 2021 12:16:49 +0200 | wenzelm | clarified signature: Bytes extends CharSequence already (see d201996f72a8); | changeset | files |
| Mon, 12 Apr 2021 11:45:16 +0200 | wenzelm | clarified exceptions; | changeset | files |
| Sun, 11 Apr 2021 22:47:55 +0200 | wenzelm | more uniform use of Byte_Message; | changeset | files |