2 months ago wenzelm 2019-06-03 tuned;
11 months ago wenzelm 2018-09-24 tuned signature;
11 months ago wenzelm 2018-08-30 tuned signature;
11 months ago wenzelm 2018-08-30 clarified signature: explicit type Locale.registration;
18 months ago wenzelm 2018-02-21 more standard instantiate operations, where substitutions are already certified and stored with trimmed theory certificate;
18 months ago wenzelm 2018-02-19 support for lazy notes in global/local context and Element.Lazy_Notes: name binding and fact without attributes; register_proofs is now based on lazy thms, but Thm.consolidate_theory will eventually force this (in parallel); support for lazy notes for locale activation (still inactive);
19 months ago ballarin 2018-01-16 Experimental support for rewrite morphisms in locale instances.
2017-08-04 haftmann 2017-08-04 provide explicit variant initializers for regular named target vs. almost-named target
2016-07-06 wenzelm 2016-07-06 tuned signature;
2016-06-23 wenzelm 2016-06-23 tuned signature;
2016-06-09 wenzelm 2016-06-09 tuned;
2016-04-11 wenzelm 2016-04-11 tuned;
2015-06-01 haftmann 2015-06-01 explicit input marker for operations
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-09 wenzelm 2014-11-09 proper context for match_tac etc.;
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-09-11 haftmann 2014-09-11 use proto_base_sort uniformly
2014-09-10 haftmann 2014-09-10 explicit check phase to guide type inference of class expression towards one single type variable
2014-09-10 haftmann 2014-09-10 tuned
2014-06-07 haftmann 2014-06-07 less baroque interface
2014-06-06 haftmann 2014-06-06 dropped obscure and unused ad-hoc before_exit hook for named targets
2014-05-09 haftmann 2014-05-09 note of_class rule for type classes in theory: useful to promote class instance proofs to locale interpretation proofs
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
2013-12-31 wenzelm 2013-12-31 made SML/NJ happy;
2013-12-25 haftmann 2013-12-25 self-contained formulation of subclass command, avoiding hard-wired Named_Target.init
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-12-13 wenzelm 2013-12-13 maintain morphism names for diagnostic purposes;
2013-07-30 wenzelm 2013-07-30 type theory is purely value-oriented;
2013-07-27 wenzelm 2013-07-27 standardized aliases;
2013-07-13 haftmann 2013-07-13 tuned variable names
2013-04-10 wenzelm 2013-04-10 more standard module name Axclass (according to file name);
2013-03-27 wenzelm 2013-03-27 tuned signature and module arrangement;
2012-04-03 wenzelm 2012-04-03 close context elements via Expression.cert/read_declaration; ensure visible context;
2012-03-14 wenzelm 2012-03-14 source positions for locale and class expressions;
2012-03-10 wenzelm 2012-03-10 tuned;
2011-11-09 wenzelm 2011-11-09 avoid separate typ_check phases, integrate into main term_check 0 instead (cf. its Syntax.check_typs in Type_Infer_Context.prepare);
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