src/Pure/meta_simplifier.ML
2006-11-28 wenzelm 2006-11-28 simplified '?' operator;
2006-11-24 wenzelm 2006-11-24 ProofContext.init;
2006-11-10 haftmann 2006-11-10 introduces canonical AList functions for loop_tacs
2006-10-11 haftmann 2006-10-11 abandoned findrep
2006-10-09 wenzelm 2006-10-09 Drule.lhs/rhs_of;
2006-09-21 wenzelm 2006-09-21 member (op =); Drule.dest_equals_rhs;
2006-09-18 wenzelm 2006-09-18 Thm.dest_arg;
2006-09-15 wenzelm 2006-09-15 rrule: maintain 'extra' field for rule that contain extra vars outside elhs; rewrite_rule_extra_vars: tuned; rewritec: omit incr_indexes in most cases, which is a big performance gain;
2006-08-03 wenzelm 2006-08-03 tuned;
2006-08-02 wenzelm 2006-08-02 normalized Proof.context/method type aliases;
2006-07-30 wenzelm 2006-07-30 Thm.adjust_maxidx;
2006-07-27 wenzelm 2006-07-27 moved Goal.norm_hhf(_protect) to meta_simplifier.ML (pervasive);
2006-07-25 wenzelm 2006-07-25 use Term.add_vars instead of obsolete term_varnames;
2006-07-18 wenzelm 2006-07-18 Term.declare_term_names;
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list); Name.bound;
2006-07-08 wenzelm 2006-07-08 tuned exception handling;
2006-07-06 wenzelm 2006-07-06 add/del_simps: warning for inactive simpset (no context); tuned;
2006-06-06 wenzelm 2006-06-06 tuned;
2006-05-11 wenzelm 2006-05-11 tuned;
2006-04-29 wenzelm 2006-04-29 tuned;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-03-21 wenzelm 2006-03-21 gen_eq_set, remove (op =);
2006-02-26 wenzelm 2006-02-26 rewrite_goals_rule_aux: actually use prems if present;
2006-02-15 wenzelm 2006-02-15 rewrite_cterm: Thm.adjust_maxidx prevents unnecessary increments on rules;
2006-02-06 wenzelm 2006-02-06 Envir.(beta_)eta_contract;
2006-01-04 nipkow 2006-01-04 trace_simp_depth_limit is 1 by default
2005-12-22 wenzelm 2005-12-22 renamed imp_cong' to imp_cong_rule;
2005-11-19 wenzelm 2005-11-19 simpset: added reorient field, set_reorient;
2005-10-21 wenzelm 2005-10-21 moved various simplification tactics and rules to simplifier.ML;
2005-10-18 wenzelm 2005-10-18 renamed set_context to context; export theory_context; clear_ss: inherit_context; rewrite_aux etc.: theory_context;
2005-10-17 wenzelm 2005-10-17 added set/addloop' for simpset dependent loopers; simpset: added context field with the_context, set_context; added inherit_context (inherits bounds as well); removed obsolete inherit_bounds;
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
2005-09-29 wenzelm 2005-09-29 export debug_bounds;
2005-09-29 berghofe 2005-09-29 Simplifier now removes flex-flex constraints from theorem returned by prover.
2005-09-29 wenzelm 2005-09-29 removed revert_bound; added debug_bounds flag;
2005-09-23 wenzelm 2005-09-23 added mk_solver'; export revert_bounds; check_bounds if debug_simp;
2005-09-20 haftmann 2005-09-20 slight adaptions to library changes
2005-09-02 haftmann 2005-09-02 some 'assoc' etc. refactoring
2005-08-31 wenzelm 2005-08-31 refer to theory instead of low-level tsig;
2005-08-16 nipkow 2005-08-16 simp_depth warning now mod 20, not mod 10 (too often)
2005-08-01 wenzelm 2005-08-01 improved bounds: nameless Term.bound, recover names for output;
2005-07-28 wenzelm 2005-07-28 Term.bound;
2005-07-15 wenzelm 2005-07-15 tuned fold on terms;
2005-07-14 wenzelm 2005-07-14 tuned;
2005-07-13 wenzelm 2005-07-13 export eq_rrule; improved Net interface;
2005-07-01 wenzelm 2005-07-01 decomp_simp: compare terms, not cterms;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory;
2005-06-13 nipkow 2005-06-13 changed -1 back to 0
2005-06-12 nipkow 2005-06-12 simp_depth now starts at -1 to make it start at 0 ;-)
2005-06-06 nipkow 2005-06-06 Added the t = x "fix" - in (* ... *) :-(
2005-05-23 nipkow 2005-05-23 tuned trace info (depth)
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-24 berghofe 2005-01-24 Removed unnecessary subsignature checks to speed up rewriting.
2004-10-18 berghofe 2004-10-18 Replaced list of bound variables in simpset by maximal index of bound variables. This allows new variable names to be generated more quickly (without calling variant).
2004-09-11 nipkow 2004-09-11 undoing previous change
2004-09-10 nipkow 2004-09-10 new forward deduction capability for simplifier
2004-07-30 wenzelm 2004-07-30 tuned output;
2004-07-11 wenzelm 2004-07-11 improved print_ss; tuned;