src/Pure/Isar/class.ML
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
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;