replaced pprint_sg by Sign.pprint_sg; added Syntax.simple_pprint_typ;

replaced eq_sg by Sign.eq_sg;

removed eq_sg, pprint_sg, print_sg (now in sign.ML); removed cterm_fun, read_ctyp (now in thm.ML); print_theory: now shows all contents;

major cleanup; added eq_sig; added print_sg (full contents), pprint_sg (stamps only); added certify_typ, certify_term; changed read_typ: result now certified;

extend_theory: changed type of "abbrs" arg; added cterm_fun, read_ctyp (from drule.ML); ctyp_of, cterm_of, etc.: now use Sign.certify_...; assumption: now uses Envir.is_empty; bicompose_aux: fixed BUG (unifier with empty "asol" but non-empty "iTs" wasn't applied); fixed axioms_of;

made error message "file not found" more informative

case was renamed to sum_case

added is_empty: env -> bool, minidx: env -> int option;

added HOLCF

removed square and fact

HOLCF examples

Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF in HOL.

commented out sig constraint of functor (for debugging purposes);

changed SYNTAX_FILES;

contains remaining parts of xgram.ML and extension.ML; syn_ext replaces xgram and ext;

minor internal changes;

MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables now much leaner (eliminated gramgraph, all data except tables of old parser are shared); simplified the internal interfaces for syntax extension; added translations for _explode, _implode (experimental);

MAJOR INTERNAL CHANGE: extend and merge operations of syntax tables now much leaner (eliminated gramgraph, all data except tables of old parser are shared); simplified the internal interfaces for syntax extension;

added some utils: commas, breaks, fbreaks, block, parents, list, str_list;

cosmetic changes;

minor cleanup; added extend, merge; added {lookup,make,dest}_multi;

major cleanup and reorganisation; added generic_extend, generic_merge; added various minor functions;

corrected comment

Updated refs to old Sign functions