2011-04-16 wenzelm 2011-04-16 prefer local name spaces; tuned signatures; tuned;
2010-12-18 ballarin 2010-12-18 Add mixins to sublocale command.
2010-11-20 wenzelm 2010-11-20 renamed raw "explode" function to "raw_explode" to emphasize its meaning;
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-09-16 wenzelm 2010-09-16 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 haftmann 2010-09-13 more precise name for activation of improveable syntax
2010-09-05 wenzelm 2010-09-05 turned show_sorts/show_types into proper configuration options;
2010-09-05 wenzelm 2010-09-05 pretty printing: prefer regular Proof.context over Pretty.pp, which is mostly for special bootstrap purposes involving theory merge, for example;
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-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-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-11 haftmann 2010-08-11 merged
2010-08-11 haftmann 2010-08-11 tuned internal structure
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 explicit accessed to structure Class_Target
2010-08-11 wenzelm 2010-08-11 spelling;
2010-08-11 haftmann 2010-08-11 renamed Theory_Target to the more appropriate Named_Target
2010-07-31 ballarin 2010-07-31 Make registrations generic data.
2010-05-24 ballarin 2010-05-24 Reapply mixin patch: base for performance improvements.
2010-05-14 ballarin 2010-05-14 Revert mixin patch due to inacceptable performance drop.
2010-05-13 ballarin 2010-05-13 Remove improper use of mixin in class package.
2010-05-08 wenzelm 2010-05-08 tuned error message: regular Pretty.string_of instead of raw Pretty.output;
2010-05-08 wenzelm 2010-05-08 unified/simplified Pretty.margin_default; discontinued special Pretty.setmargin etc; explicit margin argument for Pretty.string_of_margin etc.;
2010-05-05 haftmann 2010-05-05 eq_morphism is always optional: avoid trivial morphism for empty list of equations
2010-05-05 haftmann 2010-05-05 tuned interpunctation, dropped dead comment
2010-05-04 wenzelm 2010-05-04 merged
2010-05-04 haftmann 2010-05-04 locale predicates of classes carry a mandatory "class" prefix
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-28 haftmann 2010-04-28 merged
2010-04-28 haftmann 2010-04-28 try to observe intended meaning of add_registration interface more closely
2010-04-28 haftmann 2010-04-28 empty class specifcations observe default sort
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-09 wenzelm 2010-03-09 added ProofContext.tsig_of -- proforma version for local name space only, not logical content; added ProofContext.read_type_name_proper; localized ProofContext.read_class/read_arity/cert_arity; localized ProofContext.class_space/type_space etc.;
2010-02-12 haftmann 2010-02-12 tuned comments
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-10 wenzelm 2009-11-10 modernized structure Theory_Target;
2009-10-25 wenzelm 2009-10-25 eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-17 wenzelm 2009-10-17 operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
2009-10-07 haftmann 2009-10-07 do not use Locale.add_registration_eqs any longer
2009-10-01 haftmann 2009-10-01 proper merge of interpretation equations
2009-09-27 haftmann 2009-09-27 dropped dead code
2009-07-25 haftmann 2009-07-25 improved handling of parameter import; tuned
2009-07-20 haftmann 2009-07-20 dropped add_registration interface in locale
2009-07-10 haftmann 2009-07-10 tuned
2009-07-06 wenzelm 2009-07-06 clarified Thm.of_class/of_sort/class_triv;
2009-07-06 wenzelm 2009-07-06 renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
2009-07-02 wenzelm 2009-07-02 renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
2009-06-24 wenzelm 2009-06-24 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported); renamed Variable.importT_thms to Variable.importT (again);
2009-06-17 haftmann 2009-06-17 skip_proof where appropriate
2009-06-15 haftmann 2009-06-15 skip_proof not operative here
2009-06-14 haftmann 2009-06-14 using skip_proof where appropriate
2009-03-28 wenzelm 2009-03-28 simplified Locale.activate operations, using generic context; misc tuning;
2009-03-28 wenzelm 2009-03-28 simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;
2009-03-19 wenzelm 2009-03-19 use Name.of_binding for basic logical entities without name space (fixes, case names etc.);
2009-03-07 wenzelm 2009-03-07 more uniform handling of binding in targets and derived elements;
2009-03-07 wenzelm 2009-03-07 Binding.str_of: removed verbose feature, include qualifier in output; renamed Binding.add_prefix to Binding.prefix;
2009-03-04 blanchet 2009-03-04 Merge.