src/Pure/Isar/class_declaration.ML
2011-11-09 wenzelm 2011-11-09 clarified singleton_fixate: intersection with supersort is identity, only replace actual type inference parameters; tuned reject_other, after_infer_fixate;
2011-11-09 wenzelm 2011-11-09 misc tuning and simplification;
2011-11-09 wenzelm 2011-11-09 tuned signature; tuned;
2011-11-09 wenzelm 2011-11-09 tuned layout;
2011-04-27 wenzelm 2011-04-27 tuned signature -- eliminated odd comment;
2011-04-19 wenzelm 2011-04-19 simplified check/uncheck interfaces: result comparison is hardwired by default; tuned;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-16 wenzelm 2011-04-16 tuned signature, disentangled dependencies;
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-10-26 haftmann 2010-10-26 consider base sorts of superclasses simultaneously during processing of class specification -- avoids clash of different base sorts
2010-08-30 wenzelm 2010-08-30 tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
2010-08-26 wenzelm 2010-08-26 renamed ProofContext.theory(_result) to ProofContext.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
2010-08-17 haftmann 2010-08-17 enforcing a singleton type inference parameter after type inference and before fixation prevents multiple type variables in import during class declaration
2010-08-13 haftmann 2010-08-13 corrected handling of `constrains` elements
2010-08-12 haftmann 2010-08-12 named target is optional
2010-08-12 haftmann 2010-08-12 Named_Target.init: empty string represents theory target
2010-08-11 haftmann 2010-08-11 merged
2010-08-11 haftmann 2010-08-11 more convenient split of class modules: class and class_declaration