src/Pure/Isar/class.ML
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.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-03 wenzelm 2009-03-03 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; minor tuning;
2009-03-03 wenzelm 2009-03-03 Thm.binding;
2009-02-06 haftmann 2009-02-06 more robust failure in error situations
2009-02-03 haftmann 2009-02-03 handling type classes without parameters
2009-02-01 haftmann 2009-02-01 proper declared constants in class expressions
2009-01-28 haftmann 2009-01-28 explicit check for exactly one type variable in class specification elements
2009-01-26 haftmann 2009-01-26 fixed reading of class specs: declare class operations in context
2009-01-26 haftmann 2009-01-26 correct proof of assm_intro rule
2009-01-23 haftmann 2009-01-23 fixed fixme
2009-01-21 haftmann 2009-01-21 no base sort in class import
2009-01-21 haftmann 2009-01-21 improved and corrected reading of class specs -- still draft version
2009-01-19 haftmann 2009-01-19 improved tackling of subclasses
2009-01-18 haftmann 2009-01-18 improved calculation of morphisms and rules
2009-01-17 haftmann 2009-01-17 code cleanup
2009-01-16 haftmann 2009-01-16 migrated class package to new locale implementation
2009-01-11 haftmann 2009-01-11 construct explicit class morphism
2009-01-07 haftmann 2009-01-07 proper local_theory after Class.class
2009-01-05 haftmann 2009-01-05 locale -> old_locale, new_locale -> locale
2009-01-05 haftmann 2009-01-05 rearranged target theories
2009-01-02 haftmann 2009-01-02 improved boostrap order: theory_target.ML before expression.ML
2008-12-17 haftmann 2008-12-17 temporary adaption to new locale code
2008-12-09 ballarin 2008-12-09 NewLocale.intro_locales_tac added to Class.default_intro_tac.
2008-12-05 haftmann 2008-12-05 Name.name_of -> Binding.base_name
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-12-01 haftmann 2008-12-01 new Binding module
2008-11-20 haftmann 2008-11-20 using name bindings
2008-11-17 haftmann 2008-11-17 explicit name morphism function for locale interpretation
2008-11-13 haftmann 2008-11-13 proper name morphisms for locales
2008-11-06 haftmann 2008-11-06 class morphism stemming from locale interpretation
2008-10-23 wenzelm 2008-10-23 renamed Thm.get_axiom_i to Thm.axiom;
2008-10-22 haftmann 2008-10-22 prove_instantiation_exit combinators
2008-09-17 ballarin 2008-09-17 Public interface to interpretation morphism.
2008-09-03 wenzelm 2008-09-03 Sign.declare_const: Name.binding;
2008-09-02 ballarin 2008-09-02 Interpretation commands no longer accept interpretation attributes.
2008-09-02 wenzelm 2008-09-02 type Attrib.binding abbreviates Name.binding without attributes; Attrib.no_binding refers to Name.no_binding;
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-08-27 wenzelm 2008-08-27 type Properties.T;
2008-08-06 ballarin 2008-08-06 Interpretation command (theory/proof context) no longer simplifies goal.
2008-07-30 haftmann 2008-07-30 improved morphism
2008-07-29 haftmann 2008-07-29 some steps towards explicit class target for canonical interpretation
2008-07-25 haftmann 2008-07-25 subclass now also works for subclasses with empty specificaton
2008-06-19 wenzelm 2008-06-19 Variable.declare_typ;
2008-06-07 haftmann 2008-06-07 fixed wrong treatment of type variables in instantiation target
2008-05-26 haftmann 2008-05-26 check for illegal merge of class parameters
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-04-29 haftmann 2008-04-29 proper input abbreviations in class
2008-04-22 haftmann 2008-04-22 proper abbreviations in class
2008-04-13 wenzelm 2008-04-13 Sorts.class_error: produce message only (formerly msg_class_error);
2008-04-12 wenzelm 2008-04-12 replaced Drule.close_derivation/Goal.close_result by Thm.close_derivation (removed obsolete compression);
2008-04-10 haftmann 2008-04-10 check validity of class target improvement
2008-04-02 haftmann 2008-04-02 improved improvements for instantiaton
2008-03-28 haftmann 2008-03-28 unfold_locales now part of default tactic
2008-03-28 wenzelm 2008-03-28 Context.>> : operate on Context.generic;
2008-03-27 wenzelm 2008-03-27 eliminated delayed theory setup
2008-03-20 haftmann 2008-03-20 (continued)
2008-03-19 haftmann 2008-03-19 instantiation less liberal with dangling constraints
2008-03-12 haftmann 2008-03-12 better improvement in instantiation target