src/Pure/General/symbol_explode.ML
Mon, 23 Aug 2021 12:25:55 +0200 wenzelm tuned;
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