1994-08-19 wenzelm 1994-08-19 added inferT_axm; removed extend_theory; changed read_def_cterm: now uses Sign.infer_types;
1994-07-20 wenzelm 1994-07-20 fixed comment: "(| _ : _ |)" to "OFCLASS(_, _)"
1994-07-01 clasohm 1994-07-01 rewritec now uses trace_thm for it's "rewrite rule from different theory" message
1994-06-20 nipkow 1994-06-20 Improved error msg "Proved wrong thm"
1994-06-17 nipkow 1994-06-17 ordered rewriting applies to conditional rules as well now
1994-06-16 wenzelm 1994-06-16 added add_classrel;
1994-05-29 nipkow 1994-05-29 Internale optimization of the simplifier: in case a subterm stays unchanged, None is returned. Speeds things up a little bit and is going to be useful later on.
1994-05-26 wenzelm 1994-05-26 added class_triv: theory -> class -> thm (for axclasses); renamed ext_axtab to new_axioms; restored functor sig constraint :THM;
1994-05-19 wenzelm 1994-05-19 new datatype theory, supports 'draft theories' and incremental extension: add_classes, add_defsort, add_types, add_tyabbrs, add_tyabbrs_i, add_arities, add_consts, add_consts_i, add_syntax, add_syntax_i, add_trfuns, add_trrules, add_axioms, add_axioms_i, add_thyname; added merge_thy_list for multiple merges and extend-merges; added rep_theory, subthy, eq_thy, cert_axm, read_axm; changed type of axioms_of; renamed internal merge_theories to merge_thm_sgs; various internal changes of thm and theory related code;
1994-04-06 lcp 1994-04-06 restored the signature constraint :THM
1994-03-27 nipkow 1994-03-27 Changed term ordering for permutative rewrites to be AC-compatible.
1994-03-22 nipkow 1994-03-22 Implemented "ordered rewriting": rules which merely permute variables, such as commutativity, are only applied if the term becaomes lexicographically smaller (according to some fixed ordering on the term structure).
1994-03-01 nipkow 1994-03-01 deleted a comment
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-01-19 wenzelm 1994-01-19 commented out sig constraint of functor (for debugging purposes);
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-14 nipkow 1994-01-14 optimized net for matching of abstractions to speed up simplifier
1994-01-11 nipkow 1994-01-11 optimized the number of eta-contractions in rewriting
1994-01-10 wenzelm 1994-01-10 commented out sig constraint of functor (for debugging purposes);
1994-01-05 nipkow 1994-01-05 added new parameter to the simplification tactics which indicates if assumptions are to be simplified and/or to be used when simplifying the conclusion. This gets rid of METAHYPS and speeds up simplification of goals with big assumptions.
1994-01-04 nipkow 1994-01-04 changed tracing of simplifier
1994-01-02 nipkow 1994-01-02 optimized simplifier - signature of rewritten term stays constant
1993-12-21 nipkow 1993-12-21 Necessary changes to accomodate type abbreviations.
1993-12-10 nipkow 1993-12-10 updated instantiate to deal with type clashes
1993-11-22 nipkow 1993-11-22 Fixed bug in rewriter (fun impc) discovered by Marcus Moore.
1993-11-11 nipkow 1993-11-11 Changed the simplifier: if the subgoaler proves an unexpected thm, chances are, it is an instance of the expected thm. Instead of aborting, rewriting now fails at that point.
1993-10-29 nipkow 1993-10-29 added function del_simps
1993-09-16 clasohm 1993-09-16 Initial revision