2005-07-28 wenzelm 2005-07-28 Sign.typ_unify;
2005-07-01 wenzelm 2005-07-01 back to 1.28;
2005-06-30 wenzelm 2005-06-30 revert to 1.27 due to obscure performance issues (!??);
2005-06-29 wenzelm 2005-06-29 pass thy as explicit argument (the old ref was not safe in conjunction with lazy evaluation -- the unify code could be fooled about the present theory context);
2005-06-17 wenzelm 2005-06-17 accomodate identification of type and theory;
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-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2004-11-11 paulson 2004-11-11 increased tracing and search bounds
2004-04-22 wenzelm 2004-04-22 tuned;
2001-12-18 wenzelm 2001-12-18 tuned Type.unify;
2001-11-21 wenzelm 2001-11-21 use tracing function for trace output;
2001-11-19 berghofe 2001-11-19 Moved head_norm and fastype from unify.ML to envir.ML
2000-03-10 berghofe 2000-03-10 Type.unify and Type.typ_match now use Vartab instead of association lists.
1997-12-19 wenzelm 1997-12-19 adapted to new sort function;
1997-11-27 wenzelm 1997-11-27 fixed warning;
1997-11-21 wenzelm 1997-11-21 changed Sequence interface (now Seq, in seq.ML);
1997-10-24 wenzelm 1997-10-24 ProtoPure.thy;
1997-03-07 paulson 1997-03-07 Removed some polymorphic equality tests
1996-11-18 paulson 1996-11-18 Changed subst_bounds to subst_bound, to run faster
1996-11-12 paulson 1996-11-12 Changed some mem calls to be monomorphic
1996-10-30 paulson 1996-10-30 Changed some mem calls to mem_int for greater efficiency (not that it could matter)
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
1996-01-11 nipkow 1996-01-11 Removed bug in type unification. Negative indexes are not used any longer. Had to change interface to Type.unify to pass maxidx. Thus changes in the clients.
1995-03-03 clasohm 1995-03-03 added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1994-10-21 lcp 1994-10-21 Pure/Unify/IMPROVING "CLEANING" OF FLEX-FLEX PAIRS: Old code would refuse to simplfy %x y.?a(x) =?= %x y.?b(f(?c(y), y)) because it found the flexible path to y before the rigid path. New code simplifies this to %x.?a(x) =?= %x.?d, eliminating ?a. Pure/Unify/rigid_bound: preliminary check for rigid paths to the banned bound variables Pure/Unify/change_bnos: any occurrences of the banned bound variables must now be flexible, causing abandonment of the "cleaning"
1994-10-19 lcp 1994-10-19 new comments explaining abandoned change
1993-09-16 clasohm 1993-09-16 Initial revision