src/Pure/raw_simplifier.ML
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;
2012-02-14 wenzelm 2012-02-14 tuned signature;
2012-02-14 wenzelm 2012-02-14 eliminated unused rewrite_goal_rule;
2012-02-14 wenzelm 2012-02-14 eliminated obsolete aliases;
2012-01-11 wenzelm 2012-01-11 more qualified names; more antiquotations;
2011-11-24 wenzelm 2011-11-24 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-11-23 wenzelm 2011-11-23 tuned;
2011-11-23 wenzelm 2011-11-23 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-11-08 wenzelm 2011-11-08 eliminated obsolete tuning (NB: Thm.eta_conversion/Envir.eta_contract based on Same.operation);
2011-10-28 wenzelm 2011-10-28 tuned signature -- refined terminology;
2011-08-08 wenzelm 2011-08-08 misc tuning -- eliminated old-fashioned rep_thm;
2011-06-29 wenzelm 2011-06-29 tuned signature;
2011-06-29 wenzelm 2011-06-29 simplified/unified Simplifier.mk_solver;
2011-06-09 wenzelm 2011-06-09 simplified Name.variant -- discontinued builtin fold_map;
2011-04-22 wenzelm 2011-04-22 tuned signature;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-01-08 wenzelm 2011-01-08 tuned;