src/Pure/raw_simplifier.ML
20 months ago nipkow 2017-10-29 reduced simp_depth_limit
2016-12-13 wenzelm 2016-12-13 more symbols;
2016-06-02 wenzelm 2016-06-02 avoid warnings on duplicate rules in the given list;
2016-04-08 wenzelm 2016-04-08 eliminated unused simproc identifier;
2016-04-05 wenzelm 2016-04-05 clarified modules -- simplified bootstrap;
2015-08-31 wenzelm 2015-08-31 routine check of theory context;
2015-09-09 wenzelm 2015-09-09 simplified simproc programming interfaces;
2015-09-02 wenzelm 2015-09-02 eliminated pointless cterms;
2015-09-02 wenzelm 2015-09-02 trim context for persistent storage;
2015-09-02 wenzelm 2015-09-02 more thorough transfer;
2015-08-30 wenzelm 2015-08-30 trim context for persistent storage;
2015-07-28 wenzelm 2015-07-28 more explicit context;
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-06-01 wenzelm 2015-06-01 tuned;
2015-05-12 nipkow 2015-05-12 this warning is hardly useful but produces noisy markers in the jedit interface
2015-03-13 nipkow 2015-03-13 rhs of eqn is only eta- but not beta-eta-contracted; hence the latter is performed explicitly if needed
2015-03-07 wenzelm 2015-03-07 clarified Drule.gen_all: observe context more carefully;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 clarified signature;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-08 wenzelm 2014-11-08 optional proof context for unify operations, for the sake of proper local options;
2014-11-01 wenzelm 2014-11-01 eliminated former Proof General preferences;
2014-10-30 wenzelm 2014-10-30 tuned spelling;
2014-08-05 wenzelm 2014-08-05 more careful treatment of context visibility for rule declarations (see also 39d9c7f175e0, e639d91d9073) -- avoid duplicate warnings;
2014-04-06 wenzelm 2014-04-06 more source positions;
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-02-20 wenzelm 2014-02-20 tuned signature; tuned message;
2014-02-10 wenzelm 2014-02-10 more elementary put_simpset: exchange the simplifier configuration outright, which is particularly relevant concerning cumulative depth, e.g. for Product_Type.split_beta in the subsequent example: lemma "P (\<lambda>s. (case s of (x, y) \<Rightarrow> c))" using [[simp_depth_limit = 1]] apply simp oops
2014-02-04 Lars Hupel 2014-02-04 interactive simplifier trace: new panel in Isabelle/jEdit to inspect and modify simplification state
2014-01-17 wenzelm 2014-01-17 back to conditional tracing instead of noisy warning (see also 00e849f5b397): these incidents happen occasionally;
2014-01-17 wenzelm 2014-01-17 tuned;
2014-01-17 wenzelm 2014-01-17 clarified Simplifier diagnostics -- simplified ML; unconditional warning for structural mistakes (NB: context of running Simplifier is not visible, and cond_warning ineffective);
2014-01-15 wenzelm 2014-01-15 general notion of auxiliary bounds within context; revert_bounds as part of regular unparse_term; avoid special variants of Syntax.string_of_term in Simplifier (e.g. relevant for add-on tracing);
2014-01-12 wenzelm 2014-01-12 proper context for clear_simpset: preserve dounds, depth; dismantled obsolete debug_bounds/check_bounds;
2014-01-12 wenzelm 2014-01-12 tuned signature;
2014-01-10 wenzelm 2014-01-10 more elementary management of declared hyps, below structure Assumption; Goal.prove: insist in declared hyps; Simplifier: declare hyps via Thm.assume_hyps; more accurate tool context in some boundary cases;
2014-01-10 wenzelm 2014-01-10 tuned;
2014-01-01 wenzelm 2014-01-01 clarified simplifier context; eliminated Simplifier.global_context;
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-12-12 wenzelm 2013-12-12 clarified Trace_Ops: global theory data avoids init of simpset in Pure.thy, which is important to act as neutral element in merge;
2013-12-12 wenzelm 2013-12-12 generic trace operations for main steps of Simplifier;
2013-12-12 wenzelm 2013-12-12 tuned signature;
2013-12-12 wenzelm 2013-12-12 tuned whitespace;
2013-12-12 wenzelm 2013-12-12 tuned whitespace;
2013-12-12 wenzelm 2013-12-12 removed dead code -- ctxt is never visible (see also 658fcba35ed7);
2013-05-30 wenzelm 2013-05-30 tuned signature;
2013-05-20 wenzelm 2013-05-20 more rigorous check of simplifier context; tuned;
2013-05-20 wenzelm 2013-05-20 tuned;
2013-05-16 wenzelm 2013-05-16 tuned signature -- depend on context by default;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-04 nipkow 2013-04-04 removed unnerving (esp in jedit) and pointless warning
2013-03-30 wenzelm 2013-03-30 amended uncond_skel to observe notion of cong_name properly -- may affect simplification with Free congs;
2013-03-30 wenzelm 2013-03-30 more formal cong_name;
2012-09-29 wenzelm 2012-09-29 more explicit Syntax_Trans.mark_bound_abs/mark_bound_body: preserve type information for show_markup;
2012-08-29 wenzelm 2012-08-29 renamed Position.str_of to Position.here;
2012-03-31 wenzelm 2012-03-31 tuned signature;
2012-02-27 wenzelm 2012-02-27 eliminated odd comment from distant past;