2010-06-01 ago do not expose store flag of AxClass.add_*
2010-06-01 ago merged
2010-06-01 ago classrel and arity theorems are now stored under proper name in theory. add_arity and
2010-05-27 ago renamed structure PrintMode to Print_Mode, keeping the old name as legacy alias for some time;
2010-05-27 ago renamed structure TypeInfer to Type_Infer, keeping the old name as legacy alias for some time;
2010-05-05 ago eq_morphism is always optional: avoid trivial morphism for empty list of equations
2010-05-05 ago tuned interpunctation, dropped dead comment
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-28 ago codified comment
2010-04-25 ago replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
2010-04-25 ago modernized naming conventions of main Isar proof elements;
2010-04-11 ago Thm.add_axiom/add_def: return internal name of foundational axiom;
2010-03-21 ago handle hidden polymorphism in class target (without class target syntax, though)
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-09 ago added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
2010-02-23 ago dropped axclass
2010-02-15 ago clarifed type
2010-02-07 ago renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2009-11-30 ago dropped some unused bindings
2009-11-30 ago more accurate linerarity
2009-11-13 ago modernized structure Local_Theory;
2009-11-08 ago adapted Theory_Data;
2009-11-08 ago adapted Generic_Data, Proof_Data;
2009-10-25 ago eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-17 ago operations of structure Skip_Proof (formerly SkipProof) no longer require quick_and_dirty mode;
2009-10-17 ago indicate CRITICAL nature of various setmp combinators;
2009-10-01 ago proper merge of interpretation equations
2009-10-01 ago Merged.
2009-08-19 ago Improved comments and api names.
2009-08-15 ago additional checkpoints avoid problems in error situations
2009-07-15 ago simplification of locale interfaces
2009-07-10 ago tuned locale interface
2009-06-29 ago mutual instances
2009-06-17 ago stripped dead comment
2009-06-14 ago axclass command now legacy
2009-06-09 ago tuned make/map/merge combinators
2009-05-24 ago tuned class user space type system code
2009-05-20 ago tuned
2009-05-20 ago avoid potential problem with stale theory
2009-04-28 ago prevent potential failure
2009-03-28 ago simplified Locale.activate operations, using generic context;
2009-03-13 ago merged
2009-03-13 ago coherent binding policy with primitive target operations
2009-03-13 ago simplified method setup;
2009-03-13 ago unified type Proof.method and pervasive METHOD combinators;
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-07 ago more uniform handling of binding in targets and derived elements;
2009-03-05 ago renamed NameSpace.base to NameSpace.base_name;
2009-02-18 ago more precise improvement in instantiation user space type system
2009-01-26 ago fixed reading of class specs: declare class operations in context
2009-01-21 ago allow empty class specs
2009-01-21 ago code cleanup
2009-01-19 ago improved tackling of subclasses
2009-01-17 ago tuned signature
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-06 ago locale -> old_locale, new_locale -> locale
2009-01-05 ago locale -> old_locale, new_locale -> locale
2009-01-05 ago rearranged target theories