src/Pure/envir.ML
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