src/HOL/ex/ML.thy
2016-04-07 wenzelm 2016-04-07 explicit handling of recursive ML name space, e.g. relevant for ML_Bootstrap; handle bootstrap signatures as well;
2015-11-30 wenzelm 2015-11-30 tuned;
2014-11-02 wenzelm 2014-11-02 modernized header uniformly as section;
2014-10-07 wenzelm 2014-10-07 more cartouches;
2014-03-25 wenzelm 2014-03-25 clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);
2014-03-02 wenzelm 2014-03-02 clarified names of antiquotations and markup; more documentation;
2013-12-09 wenzelm 2013-12-09 more antiquotations;
2013-09-27 wenzelm 2013-09-27 proper latex;
2013-09-26 wenzelm 2013-09-26 added Isabelle/ML example;