src/Tools/code/code_target.ML
Fri, 26 Oct 2007 19:58:32 +0200 wenzelm replaced Secure.evaluate by ML_Context.evaluate;
less more (0) -10 -1 tip