src/Pure/envir.ML
2007-09-21 wenzelm 2007-09-21 Term.has_abs;
2007-04-14 wenzelm 2007-04-14 Term.string_of_vname;
2007-01-24 wenzelm 2007-01-24 tuned eta_contract;
2006-12-12 wenzelm 2006-12-12 added expand_term_frees;
2006-12-07 wenzelm 2006-12-07 added expand_term;
2006-09-21 wenzelm 2006-09-21 tuned eta_contract;
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-07-11 wenzelm 2006-07-11 removed obsolete xless;
2006-06-12 wenzelm 2006-06-12 tuned Seq/Envir/Unify interfaces;
2006-04-13 wenzelm 2006-04-13 expand_atom: Type.raw_match;
2006-02-06 wenzelm 2006-02-06 added (beta_)eta_contract (from pattern.ML); added expand_atom;
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-07-01 berghofe 2005-07-01 Fixed bug: lookup' must use = instead of eq_type to compare types of variables, otherwise pattern matching algorithm may loop.
2005-04-21 berghofe 2005-04-21 - Eliminated nodup_vars check. - Unification and matching functions now check types of term variables / sorts of type variables when applying a substitution. - Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list as argument, to allow for proper instantiation of theorems containing type variables with same name but different sorts.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2001-12-14 wenzelm 2001-12-14 added type_env function; let norm_type_XXX work directly with type env component;
2001-11-19 berghofe 2001-11-19 Moved head_norm and fastype from unify.ML to envir.ML
2001-08-31 berghofe 2001-08-31 - exported SAME exception - exported functions for normalizing types
2000-11-17 wenzelm 2000-11-17 added beta_norm; tuned;
2000-03-10 berghofe 2000-03-10 Envir now uses Vartab instead of association lists.
1998-08-10 wenzelm 1998-08-10 fixed comment;
1996-11-18 paulson 1996-11-18 Speedups involving norm
1996-11-13 paulson 1996-11-13 In-lined the one function call to normTsh
1996-11-01 paulson 1996-11-01 Deleted Olist constructor. Replaced minidx by "above" function
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.
1996-01-29 clasohm 1996-01-29 inserted tabs again
1996-01-29 clasohm 1996-01-29 removed tabs
1994-11-21 lcp 1994-11-21 Pure/envir/norm_term: replaced equality test for [] by null
1994-01-24 wenzelm 1994-01-24 added is_empty: env -> bool, minidx: env -> int option;
1993-09-16 clasohm 1993-09-16 Initial revision