src/Pure/ML-Systems/use_context.ML
Mon, 23 Mar 2009 21:40:11 +0100 wenzelm more systematic type use_context, with particular values ML_Parse.global_context and ML_Context.local_context;
less more (0) tip