src/Pure/General/markup.ML
Sat, 07 Jul 2007 00:17:10 +0200 Common markup elements.