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
2009-01-21 ago no base sort in class import
2009-01-21 ago improved and corrected reading of class specs -- still draft version
2009-01-19 ago improved tackling of subclasses
2009-01-18 ago improved calculation of morphisms and rules
2009-01-17 ago code cleanup
2009-01-16 ago migrated class package to new locale implementation
2009-01-11 ago construct explicit class morphism
2009-01-07 ago proper local_theory after Class.class
2009-01-05 ago locale -> old_locale, new_locale -> locale
2009-01-05 ago rearranged target theories
2009-01-02 ago improved boostrap order: theory_target.ML before expression.ML
2008-12-17 ago temporary adaption to new locale code
2008-12-09 ago NewLocale.intro_locales_tac added to Class.default_intro_tac.
2008-12-05 ago Name.name_of -> Binding.base_name
2008-12-04 ago cleaned up binding module and related code
2008-12-01 ago new Binding module
2008-11-20 ago using name bindings
2008-11-17 ago explicit name morphism function for locale interpretation
2008-11-13 ago proper name morphisms for locales
2008-11-06 ago class morphism stemming from locale interpretation
2008-10-23 ago renamed Thm.get_axiom_i to Thm.axiom;
2008-10-22 ago prove_instantiation_exit combinators
2008-09-17 ago Public interface to interpretation morphism.
2008-09-03 ago Sign.declare_const: Name.binding;
2008-09-02 ago Interpretation commands no longer accept interpretation attributes.
2008-09-02 ago type Attrib.binding abbreviates Name.binding without attributes;
2008-09-02 ago explicit type Name.binding for higher-specification elements;
2008-08-27 ago type Properties.T;
2008-08-06 ago Interpretation command (theory/proof context) no longer simplifies goal.
2008-07-30 ago improved morphism
2008-07-29 ago some steps towards explicit class target for canonical interpretation
2008-07-25 ago subclass now also works for subclasses with empty specificaton