src/Pure/Isar/named_target.ML
2011-03-13 wenzelm 2011-03-13 tuned headers;
2011-01-16 wenzelm 2011-01-16 added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
2010-11-28 wenzelm 2010-11-28 superficial tuning;
2010-09-22 haftmann 2010-09-22 tuned
2010-09-20 wenzelm 2010-09-20 renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-08-26 wenzelm 2010-08-26 renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
2010-08-20 haftmann 2010-08-20 tuned: less formal noise in Named_Target, more coherence in Class
2010-08-12 haftmann 2010-08-12 Class.declare -> Class.const
2010-08-12 haftmann 2010-08-12 named target is optional; explicit Name_Target.reinit
2010-08-12 haftmann 2010-08-12 Named_Target.init: empty string represents theory target
2010-08-12 haftmann 2010-08-12 Named_Target.theory_init
2010-08-11 haftmann 2010-08-11 remove reinit operation alltogether
2010-08-11 haftmann 2010-08-11 more convenient split of class modules: class and class_declaration
2010-08-11 haftmann 2010-08-11 tuned
2010-08-11 haftmann 2010-08-11 renamed Theory_Target to the more appropriate Named_Target