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;
less more (0) -3 tip