2001-10-12 wenzelm 2001-10-12 removed lookups count; always try headless rules;
2001-01-16 wenzelm 2001-01-16 export fold_ast etc.;
2000-07-16 wenzelm 2000-07-16 AST translation rules no longer require constant head on LHS;
2000-05-30 wenzelm 2000-05-30 renamed trace/stat_norm_ast to trace/stat_ast;
1998-10-20 wenzelm 1998-10-20 simple Env replaced by Symtab;
1997-10-06 wenzelm 1997-10-06 eliminated raise_ast;
1996-11-26 paulson 1996-11-26 Eta-expansion of a function definition, for value polymorphism
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.
1995-05-26 wenzelm 1995-05-26 changed macro expander such that patterns also match prefixes of appls;
1995-03-03 clasohm 1995-03-03 added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1994-08-12 lcp 1994-08-12 updated reference to parents
1994-02-03 wenzelm 1994-02-03 minor internal changes;
1994-01-19 wenzelm 1994-01-19 cosmetic changes;
1993-10-04 wenzelm 1993-10-04 lots of internal cleaning and tuning; removed {parse,print}_{pre,post}_proc; new lexer: now human readable due to scanner combinators; new parser installed, but still inactive (due to grammar ambiguities); added Syntax.test_read; typ_of_term: sorts now made distinct and sorted; mixfix: added forced line breaks (//); PROP now printed before subterm of type prop with non-const head;
1993-09-16 clasohm 1993-09-16 Initial revision