| Thu, 14 Apr 2016 15:33:23 +0200 | wenzelm | tuned headers; | file | diff | annotate |
| Sat, 09 Apr 2016 19:38:25 +0200 | wenzelm | proper output of markup, e.g. relevant for nested ML as used in Pure/System/bash.ML; | file | diff | annotate |
| Sat, 09 Apr 2016 16:16:05 +0200 | wenzelm | shared output primitives of physical/virtual Pure; | file | diff | annotate |