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