1994-03-17 clasohm 1994-03-17 adapted type definition to new syntax
1994-03-04 wenzelm 1994-03-04 fixed misfeature in Sign.extend: types of consts were read wrt. the new syntax;
1994-03-03 lcp 1994-03-03 changed "x" to "uu" for implicit name of the dependent type variable
1994-03-01 nipkow 1994-03-01 update towards LNCS
1994-03-01 nipkow 1994-03-01 deleted a comment
1994-02-26 nipkow 1994-02-26 *** empty log message ***
1994-02-21 wenzelm 1994-02-21 improved explode_tr;
1994-02-16 nipkow 1994-02-16 minor update because HOL-lemma changed
1994-02-16 lcp 1994-02-16 tactic/make_elim_preserve: recoded to avoid using lift_inst_rule. Instead instantiate changes the indices of V and W. tactic/cut_inst_tac: new
1994-02-16 clasohm 1994-02-16 moved 'unlink ".tmp.ML"' away from 'use ".tmp.ML"' to try to fix a bug with SML
1994-02-14 lcp 1994-02-14 double_complement_Un: new
1994-02-09 wenzelm 1994-02-09 *** empty log message ***
1994-02-08 wenzelm 1994-02-08 improved eq_sg; cosmetical change in print_sg;
1994-02-08 wenzelm 1994-02-08 added eq_set;
1994-02-04 lcp 1994-02-04 correction to cut tactics
1994-02-03 lcp 1994-02-03 no longer removes *.z
1994-02-03 lcp 1994-02-03 now makes HOLCF
1994-02-03 wenzelm 1994-02-03 added strs, big_list, writeln;
1994-02-03 wenzelm 1994-02-03 added simple_string_of_typ, simple_pprint_typ; various internal changes;
1994-02-03 wenzelm 1994-02-03 added type 'syntax'; added syntax_consts (_K, _explode, _implode, ...);
1994-02-03 wenzelm 1994-02-03 minor internal changes;
1994-02-03 wenzelm 1994-02-03 syntax for type abbreviations;
1994-02-03 wenzelm 1994-02-03 (this is a preliminary release) type abbreviations;
1994-02-03 wenzelm 1994-02-03 added if_none, parents, commas, gen_duplicates, duplicates, assoc2; changed cat_lines: no final "\n";
1994-02-03 wenzelm 1994-02-03 replaced pprint_sg by Sign.pprint_sg; added Syntax.simple_pprint_typ;
1994-02-03 wenzelm 1994-02-03 replaced eq_sg by Sign.eq_sg;
1994-02-03 wenzelm 1994-02-03 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;
1994-02-03 wenzelm 1994-02-03 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;
1994-02-03 wenzelm 1994-02-03 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;
1994-02-02 clasohm 1994-02-02 made error message "file not found" more informative
1994-01-26 nipkow 1994-01-26 case was renamed to sum_case
1994-01-24 wenzelm 1994-01-24 added is_empty: env -> bool, minidx: env -> int option;
1994-01-20 nipkow 1994-01-20 added HOLCF
1994-01-20 nipkow 1994-01-20 removed square and fact
1994-01-19 nipkow 1994-01-19 HOLCF examples
1994-01-19 nipkow 1994-01-19 Franz Regensburger's Higher-Order Logic of Computable Functions embedding LCF in HOL.
1994-01-19 wenzelm 1994-01-19 commented out sig constraint of functor (for debugging purposes);
1994-01-19 wenzelm 1994-01-19 changed SYNTAX_FILES;
1994-01-19 wenzelm 1994-01-19 contains remaining parts of xgram.ML and extension.ML; syn_ext replaces xgram and ext;
1994-01-19 wenzelm 1994-01-19 minor internal changes;
1994-01-19 wenzelm 1994-01-19 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);
1994-01-19 wenzelm 1994-01-19 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;
1994-01-19 wenzelm 1994-01-19 added some utils: commas, breaks, fbreaks, block, parents, list, str_list;
1994-01-19 wenzelm 1994-01-19 cosmetic changes;
1994-01-19 wenzelm 1994-01-19 minor cleanup; added extend, merge; added {lookup,make,dest}_multi;
1994-01-19 wenzelm 1994-01-19 major cleanup and reorganisation; added generic_extend, generic_merge; added various minor functions;
1994-01-18 lcp 1994-01-18 corrected comment
1994-01-18 lcp 1994-01-18 Updated refs to old Sign functions
1994-01-18 lcp 1994-01-18 Many other files modified as follows: s|Sign.cterm|cterm|g s|Sign.ctyp|ctyp|g s|Sign.rep_cterm|rep_cterm|g s|Sign.rep_ctyp|rep_ctyp|g s|Sign.pprint_cterm|pprint_cterm|g s|Sign.pprint_ctyp|pprint_ctyp|g s|Sign.string_of_cterm|string_of_cterm|g s|Sign.string_of_ctyp|string_of_ctyp|g s|Sign.term_of|term_of|g s|Sign.typ_of|typ_of|g s|Sign.read_cterm|read_cterm|g s|Sign.read_insts|read_insts|g s|Sign.cfun|cterm_fun|g
1994-01-18 lcp 1994-01-18 Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated functions from sign.ML to thm.ML or drule.ML. This allows the "prop" field of a theorem to be regarded as a cterm -- avoids expensive calls to cterm_of.
1994-01-18 nipkow 1994-01-18 some optimizations of Larry's
1994-01-14 lcp 1994-01-14 corrected comments
1994-01-14 lcp 1994-01-14 corrected comments
1994-01-14 nipkow 1994-01-14 optimized net for matching of abstractions to speed up simplifier
1994-01-11 nipkow 1994-01-11 moved misplaced comment
1994-01-11 wenzelm 1994-01-11 removed Syntax/parse_tree.ML;
1994-01-11 nipkow 1994-01-11 optimized the number of eta-contractions in rewriting
1994-01-10 clasohm 1994-01-10 added a check for existence of a temporary file before removing it
1994-01-10 clasohm 1994-01-10 used unlink for delete_files instead of calling rm
1994-01-10 wenzelm 1994-01-10 commented out sig constraint of functor (for debugging purposes);