src/Pure/General/markup.ML
Sat, 07 Jul 2007 18:47:47 +0200 wenzelm make smlnj happy;
Sat, 07 Jul 2007 18:39:17 +0200 wenzelm added toplevel markup;
Sat, 07 Jul 2007 12:16:14 +0200 wenzelm position: line and name;
Sat, 07 Jul 2007 00:17:10 +0200 wenzelm Common markup elements.
less more (0) tip