2011-11-09 ago tuned signature;
2011-11-06 ago tuned;
2011-11-05 ago added Logic.varify_types_global/unvarify_types_global, which avoids somewhat expensive Term.map_types;
2011-10-30 ago removed obsolete argument (cf. aa35859c8741);
2011-10-28 ago refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
2011-10-28 ago uniform Local_Theory.declaration with explicit params;
2011-06-09 ago tuned signature: Name.invent and Name.invent_names;
2011-04-19 ago simplified check/uncheck interfaces: result comparison is hardwired by default;
2011-04-18 ago standardized aliases of operations on tsig;
2011-04-18 ago pass plain Proof.context for pretty printing;
2011-04-18 ago simplified Sorts.class_error: plain Proof.context;
2011-04-18 ago simplified pretty printing context, which is only required for certain kernel operations;
2011-04-17 ago report Name_Space.declare/define, relatively to context;
2011-04-16 ago modernized structure Proof_Context;
2011-04-16 ago prefer local name spaces;
2010-12-18 ago Add mixins to sublocale command.
2010-11-20 ago renamed raw "explode" function to "raw_explode" to emphasize its meaning;
2010-09-20 ago renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
2010-09-16 ago Isar "default" step needs to fail for solved problems, for clear distinction of '.' and '..' for example -- amending lapse introduced in 9de4d64eee3b (April 2004);
2010-09-13 ago more precise name for activation of improveable syntax
2010-09-05 ago turned show_sorts/show_types into proper configuration options;
2010-09-05 ago pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
2010-08-26 ago 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-26 ago 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-20 ago tuned: less formal noise in Named_Target, more coherence in Class
2010-08-12 ago Class.declare -> Class.const
2010-08-11 ago merged
2010-08-11 ago tuned internal structure
2010-08-11 ago remove reinit operation alltogether
2010-08-11 ago more convenient split of class modules: class and class_declaration
2010-08-11 ago explicit accessed to structure Class_Target
2010-08-11 ago spelling;
2010-08-11 ago renamed Theory_Target to the more appropriate Named_Target
2010-07-31 ago Make registrations generic data.
2010-05-24 ago Reapply mixin patch: base for performance improvements.
2010-05-14 ago Revert mixin patch due to inacceptable performance drop.
2010-05-13 ago Remove improper use of mixin in class package.
2010-05-08 ago tuned error message: regular Pretty.string_of instead of raw Pretty.output;
2010-05-08 ago unified/simplified Pretty.margin_default;
2010-05-05 ago eq_morphism is always optional: avoid trivial morphism for empty list of equations
2010-05-05 ago tuned interpunctation, dropped dead comment
2010-05-04 ago merged
2010-05-04 ago locale predicates of classes carry a mandatory "class" prefix
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-28 ago merged
2010-04-28 ago try to observe intended meaning of add_registration interface more closely
2010-04-28 ago empty class specifcations observe default sort
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-09 ago added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
2010-02-12 ago tuned comments
2010-02-07 ago renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-13 ago modernized structure Local_Theory;
2009-11-10 ago modernized structure Theory_Target;
2009-10-25 ago eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-17 ago operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
2009-10-07 ago do not use Locale.add_registration_eqs any longer
2009-10-01 ago proper merge of interpretation equations
2009-09-27 ago dropped dead code
2009-07-25 ago improved handling of parameter import; tuned
2009-07-20 ago dropped add_registration interface in locale