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
2009-07-10 ago tuned
2009-07-06 ago clarified Thm.of_class/of_sort/class_triv;
2009-07-06 ago renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
2009-07-02 ago renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
2009-06-24 ago renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported);
2009-06-17 ago skip_proof where appropriate
2009-06-15 ago skip_proof not operative here
2009-06-14 ago using skip_proof where appropriate
2009-03-28 ago simplified Locale.activate operations, using generic context;
2009-03-28 ago simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
2009-03-19 ago use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
2009-03-07 ago more uniform handling of binding in targets and derived elements;
2009-03-07 ago Binding.str_of: removed verbose feature, include qualifier in output;
2009-03-04 ago Merge.
2009-03-04 ago Merge.
2009-03-03 ago renamed Binding.name_pos to Binding.make, renamed Binding.base_name to Binding.name_of, renamed Binding.map_base to Binding.map_name, added mandatory flag to Binding.qualify;
2009-03-03 ago Thm.binding;
2009-02-06 ago more robust failure in error situations
2009-02-03 ago handling type classes without parameters
2009-02-01 ago proper declared constants in class expressions
2009-01-28 ago explicit check for exactly one type variable in class specification elements
2009-01-26 ago fixed reading of class specs: declare class operations in context
2009-01-26 ago correct proof of assm_intro rule
2009-01-23 ago fixed fixme