src/Pure/meta_simplifier.ML
2007-08-02 wenzelm 2007-08-02 turned simp_depth_limit into configuration option;
2007-07-23 wenzelm 2007-07-23 depth flag: plain bool ref; eliminated transform_failure (to avoid critical section for main transactions);
2007-07-05 wenzelm 2007-07-05 tuned;
2007-07-05 wenzelm 2007-07-05 tuned goal conversion interfaces;
2007-07-03 wenzelm 2007-07-03 moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
2007-06-03 wenzelm 2007-06-03 merge_ss: plain merge of prems;
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2007-05-10 wenzelm 2007-05-10 moved some Drule operations to Thm (see more_thm.ML);
2007-05-09 wenzelm 2007-05-09 simp_depth: now proper value in simpset (prevents problems with lost exception trace, enables multi-threaded simplification); trace_simp_depth_limit_exceeded: attempt to hide destructive pointer programming within simpset;
2007-04-16 haftmann 2007-04-16 canonical merge operations
2007-04-14 wenzelm 2007-04-14 Morphism.transform/form;
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-02-06 wenzelm 2007-02-06 trace/debug: avoid eager string concatenation;
2007-02-04 wenzelm 2007-02-04 type simproc: explicitl dependency of morphism; added eq_simproc, morph_simproc; renamed mk_simproc' to make_simproc -- primary interface;
2007-01-31 haftmann 2007-01-31 changed cong alist - now using AList operations instead of overwrite_warn
2007-01-04 wenzelm 2007-01-04 added mk_simproc': tuned interface; tuned runtime context: merge with dynamic one;
2006-12-30 wenzelm 2006-12-30 removed conditional combinator;
2006-12-07 wenzelm 2006-12-07 reorganized structure Tactic vs. MetaSimplifier;
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
2006-11-30 wenzelm 2006-11-30 qualified MetaSimplifier.norm_hhf(_protect);
2006-11-29 wenzelm 2006-11-29 simplified Logic.count_prems;
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;