clarified modules;

clarified signature: more types;

more symbols;

replaced the confusing int parameter by bool

removed some add-ons from modules that are relevant for the inference kernel;

optional proof context for unify operations, for the sake of proper local options;

eliminated former Proof General preferences;

more source positions;

turned pattern unify flag into configuration option (global only);

backout 3b9c31867707 -- too risky to "amend" modules from 25 years ago that don't handle Vars with different types;

more thorough type unification: treat equal Vars like other atoms, otherwise unify type of term pair (not just accidental body_type of its head Vars);

proper internal error, not user error;

tuned signature;

tuned;

unify types of bound variables in the same manner as Unify.new_dpair (which emphatically "Tries to unify types of the bound variables!");

re-use Pattern.unify_types, including its trace_unify_fail option;

tuned signature;
tuned comments;

clarified Pattern.matchess;

discontinued old-style Term.list_abs in favour of plain Term.abs;

added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;

eliminated some hard tabulators (deprecated);

make two copies (!) of Library.UnequalLengths coincide with ListPair.UnequalLengths;

First-order pattern matching: catch a rogue exception (differing numbers of arguments)

modernized structure Term_Ord;

Added function rewrite_term_top for top-down rewriting.

curried inter as canonical list operation (beware of argument order)

dropped redundant gen_ prefix

replaced old_style infixes eq_set, subset, union, inter and variants by generic versions

explicit indication of Unsynchronized.ref;

tuned/modernized Envir.subst_XXX;

tuned/modernized Envir operations;

export match_rew -- useful for implementing "procs" for rewrite_term;

tuned aeconv: test plain aconv before expensive eta_contract;

moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
tuned signature of structure Term;

matchess

moved global pretty/string_of functions from Sign to Syntax;

- Removed function eta_contract_atom, which did not quite work
- Corrected and simplified function aeconv

first_order_match now only calls loose_bvar when inside an abstraction.

added downto0 (from library.ML);

Term.string_of_vname;

tuned matches_subterm;

member (op =);
tuned pattern check;

removed obsolete xless;

replaced Term.variant(list) by Name.variant(_list);
Name.bound;

added equiv;

removed matches_seq -- didn't quite work;

added matches_seq (left-to-right matching, intermediate beta-normalization);

tuned;

tuned basic list operators (flat, maps, map_filter);

subtract (op =);

moved (beta_)eta_contract to envir.ML;
tuned;

tuned interfaces to support incremental match/unify (cf. versions in type.ML);

cleaned up nth, nth_update, nth_map and nth_string functions

minor tweaks for Poplog/ML;

TableFun/Symtab: curried lookup and update;

curried_lookup/update;

refer to theory instead of low-level tsig;

nameless Term.bound;

Sign.typ_unify;
Term.bound;
tuned rewrite_term;

avoid polyeq;

Changed interface of Envir.lookup'

- 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.

Removed practically all references to Library.foldr.

Move towards standard functions.

Deleted Library.option type.

Merged in license change from Isabelle2004

avoid implicit arguments via refs;

Removed ~10000 hack in function idx that can lead to inconsistencies
when unifying terms with a large number of abstractions.

adapted tsig interface;

tuned;

Added new function eta_long.

type_of_G now applies type substitution before decomposing type.

norm_typ -> Envir.norm_type

added failure trace information to pattern unification

Changes to rewrite_term:
- now uses skeletons to speed up rewriting
- added interface for rewriting procedures

rewrite_term: Term.rename_abs;

Removed timing function.

rewrite_term: removed rew0, so no on-the-fly eta-contraction;

eta_contract with sharing (by berghofe);
rewrite_term: proper handling of Abs cong;

added rewrite_term;
tuned;
GPLed;

added beta_eta_contract;

tuned Type.unify;

Replaced devar by Envir.head_norm

Type.unify and Type.typ_match now use Vartab instead of association lists.

Eta contraction is now performed all the time during rewriting.

Tried to speed up the rewriter by eta-contracting all patterns beforehand and
by classifying each pattern as to whether it allows first-order matching.

Tried to reorganize rewriter a little. More to be done.

Avoid eta-contraction in the simplifier.
Instead the net needs to eta-contract the object.
Also added a special function loose_bvar1(i,t) in term.ML.

Corrected aeconv and exported it

Declares eta_contract_atom; fixed comment; some tidying

A bit more pattern-matching in eta_contract

Removal of needless function definition

Added some optimized versions of functions dealing with sets
(i.e. mem, ins, eq_set etc.) which do not use the polymorphic =
operator

Elimination of fully-functorial style.
Type tactic changed to a type abbrevation (from a datatype).
Constructor tactic and function apply deleted.

inserted tabs again

removed tabs

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.

term.ML: add_loose_bnos now returns a list w/o duplicates.
pattern.ML: replaced null(loose_bnos t) by loose_bvar(t,0)

Modified pattern.ML to perform proper matching of Higher-Order Patterns.
Modified thm.ML to preserve bound var names during rewriting.
Renamed eta_matches to matches.

now calls new fastype_of in three places

Initial revision