1998-08-19 paulson 1998-08-19 The warning "Rewrite rule from different theory" is ALWAYS printed, even if tracing is off.
1998-06-05 wenzelm 1998-06-05 Object.T;
1998-04-29 wenzelm 1998-04-29 tuned get_ax (uses ancestry); added get_def: theory -> xstring -> thm;
1998-04-22 nipkow 1998-04-22 Tried to speed up the rewriter by eta-contracting all patterns beforehand and by classifying each pattern as to whether it allows first-order matching.
1998-04-04 wenzelm 1998-04-04 tuned trace msgs;
1998-03-12 nipkow 1998-03-12 Made mutual simplification of prems a special case.
1998-03-10 nipkow 1998-03-10 Asm_full_simp_tac now reorients asm c = t to t = c.
1998-03-10 nipkow 1998-03-10 New simplifier flag for mutual simplification.
1998-03-06 nipkow 1998-03-06 Removed superfluous `op'
1998-03-04 nipkow 1998-03-04 Reorganized simplifier. May now reorient rules. Moved loop tests from logic to thm.
1998-02-28 nipkow 1998-02-28 Tried to reorganize rewriter a little. More to be done.
1998-01-30 wenzelm 1998-01-30 improved tracing of rewrite rule application;
1997-12-19 wenzelm 1997-12-19 Term.termless;
1997-12-12 wenzelm 1997-12-12 tuned msg;
1997-11-27 wenzelm 1997-11-27 removed read_cterms;
1997-11-26 wenzelm 1997-11-26 added crep_cterm;
1997-11-24 nipkow 1997-11-24 Added read_def_cterms for simultaneous reading/typing of terms under defaults. Redefined read_def_cterm in in terms of read_def_cterms. Deleted obsolete read_cterms. Cleaned up def of read_insts, which is not much shorter but much clearere are correcter now.
1997-11-21 wenzelm 1997-11-21 changed Sequence interface (now Seq, in seq.ML);
1997-11-20 wenzelm 1997-11-20 added transfer_sg;
1997-11-20 wenzelm 1997-11-20 tuned infer_types interface;
1997-11-06 wenzelm 1997-11-06 deriv: eliminated references to theory;
1997-11-04 wenzelm 1997-11-04 type object = exn (enhance readability);
1997-11-04 nipkow 1997-11-04 logic: loops -> rewrite_rule_ok added rewrite_rule_extra_vars thm: Rewrite rules must not introduce new type vars on rhs. This lead to an incompleteness, is now banned, and the code has been simplified.
1997-10-30 nipkow 1997-10-30 Modified trace output routines of simplifier.
1997-10-30 wenzelm 1997-10-30 tuned simp trace;
1997-10-28 wenzelm 1997-10-28 added name_of_thm; improved name_thm: does not overwrite existing name;
1997-10-24 wenzelm 1997-10-24 eq_thm (from drule.ML);
1997-10-23 wenzelm 1997-10-23 tuned;
1997-10-22 wenzelm 1997-10-22 tuned;
1997-10-21 wenzelm 1997-10-21 sg_ref: automatic adjustment of thms of draft theories;
1997-10-16 wenzelm 1997-10-16 added transfer: theory -> thm -> thm;
1997-10-16 nipkow 1997-10-16 The simplifier has been improved a little: equations s=t which used to be rejected because of looping are now treated as (s=t) == True. The latter translation must be done outside of Thm because it involves the object-logic specific True. Therefore the simple loop test has been moved from Thm to Logic.
1997-10-09 wenzelm 1997-10-09 fixed get_axiom, invoke_oracle; improved Oracle deriv;
1997-10-06 wenzelm 1997-10-06 tuned read_cterms;
1997-07-25 wenzelm 1997-07-25 added prems argument to simplification procedures;
1997-07-23 paulson 1997-07-23 Now rename_params_rule merely issues warnings--and does nothing--if the renaming cannot be performed. Previously it raised a fatal error.
1997-07-23 wenzelm 1997-07-23 improved simp tracing;
1997-07-22 wenzelm 1997-07-22 added dest_mss, merge_mss; fixed matching of simproc lhss;
1997-07-18 wenzelm 1997-07-18 tuned warning; improved comments;
1997-06-05 paulson 1997-06-05 freezeT now refers to Type.freeze_thaw
1997-04-25 wenzelm 1997-04-25 improved tmp comment;
1997-04-24 nipkow 1997-04-24 rename_params_rule used to check if the new name clashed with a free name in the whole goal state. Now checks only the subgoal concerned.
1997-04-23 wenzelm 1997-04-23 simprocs called with eta contracted subterm;
1997-04-17 wenzelm 1997-04-17 improved type check error messages;
1997-04-16 wenzelm 1997-04-16 Sorts.str_of_sort;
1997-03-14 nipkow 1997-03-14 Avoid eta-contraction in the simplifier. Instead the net needs to eta-contract the object. Also added a special function loose_bvar1(i,t) in term.ML.
1997-02-21 paulson 1997-02-21 Introduction of rotate_rule
1997-02-15 oheimb 1997-02-15 added del_congs
1997-02-14 nipkow 1997-02-14 Made troublesome simplifier warning dependent on trace_simp.
1997-01-22 nipkow 1997-01-22 Added warning msg when the simplifier cannot use a premise as a rewrite rule because it contains (type) unknowns.
1997-01-16 wenzelm 1997-01-16 added termless parameter; added simplification procedures;
1996-12-13 wenzelm 1996-12-13 fixed warning;
1996-11-28 paulson 1996-11-28 Replaced map...~~ by
1996-11-18 paulson 1996-11-18 Changed subst_bounds to subst_bound, to run faster
1996-11-13 paulson 1996-11-13 Removal of polymorphic equality via mem, subset, eq_set, etc
1996-11-12 paulson 1996-11-12 Changed some mem, ins and union calls to be monomorphic
1996-11-06 wenzelm 1996-11-06 tuned fix_shyps a little bit more;
1996-11-01 paulson 1996-11-01 Now uses Int.max instead of max nodup_Vars now updates maxidx
1996-10-30 paulson 1996-10-30 Only calls nodup_Vars if really necessary. We get a speedup of nearly 6%
1996-10-01 wenzelm 1996-10-01 added shyps comment;