src/Pure/ML/ml_recursive.ML
Thu, 07 Apr 2016 21:27:17 +0200 wenzelm explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap;
less more (0) tip