src/Pure/General/print_mode.ML
Tue, 17 Jul 2007 13:19:39 +0200 wenzelm Generic print mode.
less more (0) tip