src/Pure/Isar/class.ML
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
2008-03-10 haftmann 2008-03-10 some theorems named explicitly
2008-03-07 haftmann 2008-03-07 generic improvable syntax for targets
2008-02-27 haftmann 2008-02-27 proper merge of base sorts
2008-01-28 wenzelm 2008-01-28 added ::: / @@@ scanner combinators;
2008-01-08 haftmann 2008-01-08 explicit type variables for instantiation
2008-01-04 haftmann 2008-01-04 improved warning
2008-01-02 haftmann 2008-01-02 clarified policy
2007-12-19 haftmann 2007-12-19 tuned primitive inferences
2007-12-17 haftmann 2007-12-17 maior tuning
2007-12-17 haftmann 2007-12-17 closed rules
2007-12-13 haftmann 2007-12-13 improved rule calculation
2007-12-11 haftmann 2007-12-11 dropped Class.prep_spec
2007-12-10 haftmann 2007-12-10 moved instance parameter management from class.ML to axclass.ML
2007-12-07 haftmann 2007-12-07 declaration of instance parameter names
2007-12-05 haftmann 2007-12-05 improved
2007-12-03 haftmann 2007-12-03 interface for unchecked definitions
2007-11-30 haftmann 2007-11-30 first working version of instance target
2007-11-29 haftmann 2007-11-29 instance command as rudimentary class target
2007-11-28 haftmann 2007-11-28 tuned interfaces of class module
2007-11-23 haftmann 2007-11-23 rudimentary instantiation target
2007-11-09 haftmann 2007-11-09 proper implementation of check phase; non-qualified names for class operations
2007-11-08 wenzelm 2007-11-08 synchronize_syntax: improved declare_const (still inactive); tuned;
2007-11-07 wenzelm 2007-11-07 refined Variable.declare_const; removed obsolete Sign.read_tyname/const (cf. ProofContext);
2007-11-06 wenzelm 2007-11-06 synchronize_syntax: declare operations within the local scope of fixes/consts (still inactive -- breaks rogue type-inference of rule_tac/where/of);
2007-11-06 haftmann 2007-11-06 Class.init now similiar to Locale.init
2007-11-02 haftmann 2007-11-02 more precise treatment of prove_subclass
2007-10-30 haftmann 2007-10-30 handling of notation in class target
2007-10-26 wenzelm 2007-10-26 export class_prefix; removed obsolete const hiding;
2007-10-26 haftmann 2007-10-26 tuned
2007-10-25 haftmann 2007-10-25 fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
2007-10-24 haftmann 2007-10-24 tuned
2007-10-22 haftmann 2007-10-22 tuned abbreviations in class context
2007-10-19 wenzelm 2007-10-19 tuned interfaces;
2007-10-19 haftmann 2007-10-19 tuned
2007-10-19 haftmann 2007-10-19 clarified abbreviations in class context
2007-10-19 ballarin 2007-10-19 Interpretation equations may have name and/or attribute.
2007-10-18 haftmann 2007-10-18 improved class syntax
2007-10-17 wenzelm 2007-10-17 removed obsolete fork_mixfix (back to theory_target.ML);
2007-10-16 haftmann 2007-10-16 global class syntax
2007-10-16 wenzelm 2007-10-16 Syntax.(un)check: explicit result option;
2007-10-15 haftmann 2007-10-15 canonical interpretation interface
2007-10-14 wenzelm 2007-10-14 added is_class; tuned signature of add_const/abbrev_in_class; removed obsolete class_of_locale/locale_of_class; tuned name prefixing: Sign.full_name does the job;
2007-10-13 wenzelm 2007-10-13 (un)overload: full rewrite; use Attrib.attribute_i for internal args; misc tuning;
2007-10-12 wenzelm 2007-10-12 fork_mixfix: explicit bool argument;
2007-10-12 haftmann 2007-10-12 tuned
2007-10-11 wenzelm 2007-10-11 dest/cert_def: replaced Pretty.pp by explicit Proof.context;
2007-10-11 wenzelm 2007-10-11 replaced Sign.add_consts_authentic by Sign.declare_const; replaced read_param by Sign.read_const, which is independent of syntax; added define_class_params (from axclass.ML);
2007-10-10 wenzelm 2007-10-10 generalized notation interface (add or del);
2007-10-09 wenzelm 2007-10-09 renamed AxClass.get_definition to AxClass.get_info (again); tuned intro_classes_tac;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;