src/Pure/General/ml_syntax.ML
Mon, 16 Apr 2007 12:16:11 +0200 wenzelm added print_indexname;
Sun, 04 Feb 2007 22:02:18 +0100 wenzelm added print_strings;
Sun, 21 Jan 2007 19:09:37 +0100 wenzelm added atomic, print_int;
Sat, 20 Jan 2007 14:09:18 +0100 wenzelm tuned;
less more (0) -4 tip