src/Pure/General/symbol_explode.ML
Thu, 22 Sep 2016 11:25:27 +0200 wenzelm discontinued raw symbols;
Wed, 21 Sep 2016 20:33:44 +0200 wenzelm more tight implementation of symbol explode operation (without support for raw symbols);
less more (0) tip