2005-03-26 ago op vor infix-Konstruktoren im datatype binding zum besseren Parsen
2005-03-17 ago added string_of_term
2005-03-10 ago Registrations of global locale interpretations: improved, better naming.
2005-03-04 ago Removed practically all references to Library.foldr.
2005-03-04 ago new first_order test
2005-03-03 ago Move towards standard functions.
2005-02-13 ago Deleted Library.option type.
2005-01-27 ago Added show_var_qmarks flag.
2004-07-08 ago added add_term_varnames, term_varnames;
2004-06-01 ago removed obsolete sort 'logic';
2004-05-29 ago moved read_int etc. to library.ML; added type 'arity';
2004-05-21 ago moved some sort ops to sorts.ML; added string_of_vname (from Syntax module);
2004-05-01 ago improved Term.invent_names;
2004-04-26 ago variant: use Symbol.bump_init;
2004-03-19 ago Removing the datatype declaration of "order" allows the standard General.order
2002-10-21 ago - removed flexpair
2002-10-14 ago Ported find_intro/elim to Isar.
2002-08-08 ago adhoc_freeze_vars;
2002-03-01 ago structure Typtab;
2002-02-28 ago added match_bvars, rename_abs (from thm.ML);
2002-02-20 ago Symbol.bump_string;
2002-01-17 ago added add_term_free_names (more precise/efficient than add_term_names);
2001-12-14 ago added invent_type_names;
2001-11-28 ago variant: preserve suffix of underscores (for skolem/internal names etc.);
2001-10-24 ago added lambda;
2001-10-23 ago replace_dummy_patterns: lift over bounds;
2001-05-31 ago invent_names
2001-01-06 ago added list_abs;
2000-12-13 ago fixed add_term_names: NameSpace.base;
2000-11-30 ago added is_replaced_dummy_pattern;
2000-08-29 ago *** empty log message ***
2000-08-04 ago added dummy_patternN, no_dummy_patterns, replace_dummy_patterns;
2000-07-13 ago add_term_consts: ins_string;
2000-03-30 ago foldl_term_types: depend on term as well;
2000-03-10 ago Added functions subst_TVars_Vartab and typ_subst_TVars_Vartab.
1999-09-29 ago added rems_sort;
1999-09-01 ago structure Termtab;
1999-08-23 ago Corrected two busg in the simplifier.
1999-07-10 ago Symtab.lookup_multi;
1999-04-30 ago val foldl_map_aterms: ('a * term -> 'a * term) -> 'a * term -> 'a * term;
1998-12-18 ago moved dest_Type to term.ML from HOL/Tools/primrec_package
1998-11-29 ago added oct_char;
1998-09-29 ago new function inter_term
1998-03-09 ago tuned some names;
1998-02-18 ago Improved loop-test for rewrite rules a little.
1998-02-12 ago tuned comments;
1998-02-06 ago added Vartab: TABLE;
1997-12-28 ago made MLWorks happy;
1997-12-28 ago renamed Symtab.null to Symtab.empty;
1997-12-24 ago export range_type;
1997-12-22 ago Added range-type for completeness
1997-12-19 ago term order;
1997-11-26 ago added foldl_atyps: ('a * typ -> 'a) -> 'a * typ -> 'a;
1997-11-07 ago changed libraray function find to find_index_eq, currying it
1997-11-07 ago added exists_Const
1997-11-01 ago New syntax function for types
1997-10-28 ago add_typ_classes, add_typ_tycons, add_term_classes, add_term_tycons,
1997-10-21 ago made Poly/ML happy, but SML/NJ unhappy;
1997-10-20 ago make SML/NJ happy;
1997-10-06 ago eliminated raise_term;