double_complement_Un: new

*** empty log message ***

improved eq_sg; cosmetical change in print_sg;

added eq_set;

correction to cut tactics

no longer removes *.z

now makes HOLCF

added strs, big_list, writeln;

added simple_string_of_typ, simple_pprint_typ; various internal changes;

added type 'syntax'; added syntax_consts (_K, _explode, _implode, ...);

minor internal changes;

syntax for type abbreviations;

(this is a preliminary release) type abbreviations;

added if_none, parents, commas, gen_duplicates, duplicates, assoc2; changed cat_lines: no final "\n";

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;