src/Pure/envir.ML
2016-08-05 wenzelm 2016-08-05 more tight filtering;
2016-08-05 wenzelm 2016-08-05 tuned;
2016-08-05 wenzelm 2016-08-05 tuned -- maxidx unused;
2016-08-05 wenzelm 2016-08-05 tuned;
2014-11-08 wenzelm 2014-11-08 clarified name of Type.unified, to emphasize its connection to the "unify" family; tuned low-level operation;
2014-11-08 wenzelm 2014-11-08 tuned;
2013-05-29 wenzelm 2013-05-29 tuned signature;
2013-05-24 wenzelm 2013-05-24 tuned;
2013-05-24 wenzelm 2013-05-24 tuned signature;
2013-05-24 wenzelm 2013-05-24 tuned signature -- slightly more general operations (cf. term.ML);
2013-05-17 wenzelm 2013-05-17 tuned signature;
2013-04-15 wenzelm 2013-04-15 make SML/NJ happy;
2013-04-12 wenzelm 2013-04-12 tuned exceptions -- avoid composing error messages in low-level situations;
2013-04-12 wenzelm 2013-04-12 tuned signature; tuned comments;
2011-06-08 wenzelm 2011-06-08 more robust exception pattern General.Subscript;
2011-03-24 wenzelm 2011-03-24 added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2009-09-30 wenzelm 2009-09-30 eliminated dead code;
2009-09-23 paulson 2009-09-23 Correct chasing of type variable instantiations during type unification. The following theory should not raise exception TERM: constdefs somepredicate :: "(('b => 'b) => ('a => 'a)) => 'a => 'b => bool" "somepredicate upd v x == True" lemma somepredicate_idI: "somepredicate id (f v) v" by (simp add: somepredicate_def) lemma somepredicate_triv: "somepredicate upd v x ==> somepredicate upd v x" by assumption lemmas somepredicate_triv [OF somepredicate_idI] lemmas st' = somepredicate_triv[where v="h :: nat => bool"] lemmas st2 = st'[OF somepredicate_idI]
2009-07-17 wenzelm 2009-07-17 tuned/modernized subst: Same.operation; renamed typ_subst_TVars to subst_type; renamed subst_TVars to subst_term_types; renamed subst_vars to subst_term; removed unused subst_Vars (covered by subst_term);
2009-07-17 wenzelm 2009-07-17 major cleanup, simplification, modernization;
2009-07-16 wenzelm 2009-07-16 use structure Same; tuned signature; tuned comments; tuned;
2009-02-27 wenzelm 2009-02-27 eliminated NJ's List.nth;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-04-13 wenzelm 2008-04-13 added insert_sorts (from thm.ML);
2008-03-19 haftmann 2008-03-19 Type.lookup now curried
2007-11-27 berghofe 2007-11-27 Optimized beta_norm: only tries to normalize term when it contains abstractions.
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