src/Pure/variable.ML
2009-09-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-07-30 wenzelm 2009-07-30 Variable.importT/import: return full instantiations, tuned;
2009-07-26 wenzelm 2009-07-26 Variable.focus: named parameters;
2009-07-09 wenzelm 2009-07-09 renamed structure TermSubst to Term_Subst;
2009-06-24 wenzelm 2009-06-24 renamed Variable.import_thms to Variable.import (back again cf. ed7aa5a350ef -- Alice is no longer supported); renamed Variable.importT_thms to Variable.importT (again);
2009-03-28 wenzelm 2009-03-28 replaced add_binds by singleton bind_term;
2009-01-21 wenzelm 2009-01-21 eliminated obsolete var morphism;
2008-12-31 wenzelm 2008-12-31 Term.declare_typ_names, Term.declare_term_frees;
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-10-16 wenzelm 2008-10-16 maintain sort occurrences of declared terms;
2008-06-19 wenzelm 2008-06-19 added declare_typ;
2008-06-10 wenzelm 2008-06-10 focus: actually declare constraints for local parameters;
2008-04-17 wenzelm 2008-04-17 variant_fixes: preserve internal state, mark skolem only for body mode; import_inst: actually observe is_open flag (cf. variant_fixes);
2007-12-07 haftmann 2007-12-07 exported declare_names
2007-11-07 wenzelm 2007-11-07 refined notion of consts within the local scope;
2007-11-06 wenzelm 2007-11-06 added is_const/declare_const for local scope of fixes/consts;
2007-10-16 wenzelm 2007-10-16 add_bind: close_schematic_term;
2007-10-04 wenzelm 2007-10-04 replaced literal 'a by Name.aT;
2007-09-29 wenzelm 2007-09-29 maintain maxidx (analogous to name context); polymorhic: observe Variable.maxidx_of;
2007-09-26 wenzelm 2007-09-26 declare_constraints: declare (fix) type variables within constraints, but not terms themselves;
2007-09-24 wenzelm 2007-09-24 added polymorphic_types;
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-15 wenzelm 2007-04-15 removed obsolete redeclare_skolems;
2007-04-15 wenzelm 2007-04-15 Thm.fold_terms;
2007-04-14 wenzelm 2007-04-14 tuned signature; export: precomputed closure, no reference to contexts;
2007-04-04 wenzelm 2007-04-04 renamed Variable.importT to importT_thms;
2007-04-03 wenzelm 2007-04-03 renamed Variable.import to import_thms (avoid clash with Alice keywords);
2006-12-12 wenzelm 2006-12-12 tuned expand_binds;
2006-12-06 wenzelm 2006-12-06 moved hidden_polymorphism to term.ML;
2006-11-28 wenzelm 2006-11-28 added add_fixed;
2006-11-24 wenzelm 2006-11-24 added export_morphism; ProofContext.init;
2006-11-14 wenzelm 2006-11-14 removed fix_frees interface; added auto_fixes (depends on body mode);
2006-11-14 wenzelm 2006-11-14 declare_constraints: reset constraint on dummyS;
2006-11-10 wenzelm 2006-11-10 tuned Variable.trade;
2006-09-30 wenzelm 2006-09-30 renamed Variable.invent_fixes to Variable.variant_fixes;
2006-09-18 wenzelm 2006-09-18 Thm.dest_arg;
2006-09-12 wenzelm 2006-09-12 moved term subst functions to TermSubst;
2006-08-02 wenzelm 2006-08-02 normalized Proof.context/method type aliases; added declare/export/import_prf; added focus_subgoal: reset/declare goal schematics;
2006-07-30 wenzelm 2006-07-30 export: refrain from adjusting maxidx;
2006-07-29 wenzelm 2006-07-29 added add_fixes_direct; tuned;
2006-07-27 wenzelm 2006-07-27 added fix_frees (from Isar/proof_context.ML);
2006-07-26 wenzelm 2006-07-26 import(T): result includes fixed types/terms; focus: tuned interface;
2006-07-25 wenzelm 2006-07-25 tuned;
2006-07-19 wenzelm 2006-07-19 reorganize declarations (more efficient); renamed rename_wrt to variant_frees (avoid confusion with Term.rename_wrt_term, which reverses the result); tuned;
2006-07-18 wenzelm 2006-07-18 added newly_fixed, focus; removed monomorphic; tuned;
2006-07-13 wenzelm 2006-07-13 Name.context already declares empty names; tune ins_sorts -- sort assigments should never change later;
2006-07-11 wenzelm 2006-07-11 separate names filed (covers fixes/defaults);
2006-07-11 wenzelm 2006-07-11 maintain Name.context for fixes/defaults; more efficient inventing/renaming of local names (cf. name.ML);
2006-07-04 wenzelm 2006-07-04 polymorphic: always generalize wrt. used_types;
2006-06-19 wenzelm 2006-06-19 added declare_thm, thm_context; added trade(T);
2006-06-17 wenzelm 2006-06-17 major reworking of export functionality -- based on Term/Thm.generalize; tuned interfaces;
2006-06-15 wenzelm 2006-06-15 Fixed type/term variables and polymorphic term abbreviations.