2007-05-07 ago simplified DataFun interfaces;
2007-04-15 ago removed obsolete redeclare_skolems;
2007-04-15 ago Thm.fold_terms;
2007-04-14 ago tuned signature;
2007-04-04 ago renamed Variable.importT to importT_thms;
2007-04-03 ago renamed Variable.import to import_thms (avoid clash with Alice keywords);
2006-12-12 ago tuned expand_binds;
2006-12-06 ago moved hidden_polymorphism to term.ML;
2006-11-28 ago added add_fixed;
2006-11-24 ago added export_morphism;
2006-11-14 ago removed fix_frees interface;
2006-11-14 ago declare_constraints: reset constraint on dummyS;
2006-11-10 ago tuned;
2006-09-30 ago renamed Variable.invent_fixes to Variable.variant_fixes;
2006-09-18 ago Thm.dest_arg;
2006-09-12 ago moved term subst functions to TermSubst;
2006-08-02 ago normalized Proof.context/method type aliases;
2006-07-30 ago export: refrain from adjusting maxidx;
2006-07-29 ago added add_fixes_direct;
2006-07-27 ago added fix_frees (from Isar/proof_context.ML);
2006-07-26 ago import(T): result includes fixed types/terms;
2006-07-25 ago tuned;
2006-07-19 ago reorganize declarations (more efficient);
2006-07-18 ago added newly_fixed, focus;
2006-07-13 ago Name.context already declares empty names;
2006-07-11 ago separate names filed (covers fixes/defaults);
2006-07-11 ago maintain Name.context for fixes/defaults;
2006-07-04 ago polymorphic: always generalize wrt. used_types;
2006-06-19 ago added declare_thm, thm_context;
2006-06-17 ago major reworking of export functionality -- based on Term/Thm.generalize;
2006-06-15 ago Fixed type/term variables and polymorphic term abbreviations.