src/Pure/Isar/class.ML
2008-03-20 ago (continued)
2008-03-19 ago instantiation less liberal with dangling constraints
2008-03-12 ago better improvement in instantiation target
2008-03-10 ago some theorems named explicitly
2008-03-07 ago generic improvable syntax for targets
2008-02-27 ago proper merge of base sorts
2008-01-28 ago added ::: / @@@ scanner combinators;
2008-01-08 ago explicit type variables for instantiation
2008-01-04 ago improved warning
2008-01-02 ago clarified policy
2007-12-19 ago tuned primitive inferences
2007-12-17 ago maior tuning
2007-12-17 ago closed rules
2007-12-13 ago improved rule calculation
2007-12-11 ago dropped Class.prep_spec
2007-12-10 ago moved instance parameter management from class.ML to axclass.ML
2007-12-07 ago declaration of instance parameter names
2007-12-05 ago improved
2007-12-03 ago interface for unchecked definitions
2007-11-30 ago first working version of instance target
2007-11-29 ago instance command as rudimentary class target
2007-11-28 ago tuned interfaces of class module
2007-11-23 ago rudimentary instantiation target
2007-11-09 ago proper implementation of check phase; non-qualified names for class operations
2007-11-08 ago synchronize_syntax: improved declare_const (still inactive);
2007-11-07 ago refined Variable.declare_const;
2007-11-06 ago synchronize_syntax: declare operations within the local scope of fixes/consts
2007-11-06 ago Class.init now similiar to Locale.init
2007-11-02 ago more precise treatment of prove_subclass
2007-10-30 ago handling of notation in class target
2007-10-26 ago export class_prefix;
2007-10-26 ago tuned
2007-10-25 ago fixed syntax; truned code structure; added primitive subclass interface with consideraton of syntax etc.
2007-10-24 ago tuned
2007-10-22 ago tuned abbreviations in class context
2007-10-19 ago tuned interfaces;
2007-10-19 ago tuned
2007-10-19 ago clarified abbreviations in class context
2007-10-19 ago Interpretation equations may have name and/or attribute.
2007-10-18 ago improved class syntax
2007-10-17 ago removed obsolete fork_mixfix (back to theory_target.ML);
2007-10-16 ago global class syntax
2007-10-16 ago Syntax.(un)check: explicit result option;
2007-10-15 ago canonical interpretation interface
2007-10-14 ago added is_class;
2007-10-13 ago (un)overload: full rewrite;
2007-10-12 ago fork_mixfix: explicit bool argument;
2007-10-12 ago tuned
2007-10-11 ago dest/cert_def: replaced Pretty.pp by explicit Proof.context;
2007-10-11 ago replaced Sign.add_consts_authentic by Sign.declare_const;
2007-10-10 ago generalized notation interface (add or del);
2007-10-09 ago renamed AxClass.get_definition to AxClass.get_info (again);
2007-10-09 ago generic Syntax.pretty/string_of operations;
2007-10-08 ago added proper subclass concept; improved class target
2007-10-08 ago added first version of user-space type system for class target
2007-10-04 ago replaced AxClass.param_tyvarname by Name.aT;
2007-10-04 ago intermediate cleanup
2007-09-30 ago Sign.add_consts_authentic: tags (Markup.property list);
2007-09-29 ago Sign.add_const_constraint;
2007-09-29 ago proper syntax during class specification