src/Pure/simplifier.ML
2016-12-13 wenzelm 2016-12-13 more symbols;
2016-07-20 wenzelm 2016-07-20 provide Pure.simp/simp_all, which only know about meta-equality;
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;
2015-12-16 wenzelm 2015-12-16 rule_attribute and declaration_attribute implicitly support abstract closure, but mixed_attribute implementations need to be aware of Thm.is_free_dummy;
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-09-09 wenzelm 2015-09-09 clarified declaration flags, like 'declaration' command;
2015-09-09 wenzelm 2015-09-09 simplified simproc programming interfaces;
2015-09-02 wenzelm 2015-09-02 eliminated pointless cterms;
2015-04-03 wenzelm 2015-04-03 more uniform "verbose" option to print name space;
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-01 wenzelm 2015-03-01 added Proof_Context.cterm_of/ctyp_of convenience;
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-10 wenzelm 2014-11-10 proper context for assume_tac (atac remains as fall-back without context);
2014-11-09 wenzelm 2014-11-09 proper context for match_tac etc.;
2014-08-27 wenzelm 2014-08-27 more explicit Method.modifier with reported position;
2014-08-19 wenzelm 2014-08-19 added PARALLEL_ALLGOALS convenience;
2014-04-10 wenzelm 2014-04-10 added simproc markup, which also indicates legacy simprocs outside the name space;
2014-03-18 wenzelm 2014-03-18 more antiquotations;
2014-03-12 wenzelm 2014-03-12 tuned signature -- clarified module name;
2014-01-12 wenzelm 2014-01-12 proper context for clear_simpset: preserve dounds, depth; dismantled obsolete debug_bounds/check_bounds;
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-11-11 wenzelm 2013-11-11 tuned signature -- removed obsolete Addsimprocs, Delsimprocs;
2013-08-23 wenzelm 2013-08-23 added Theory.setup convenience;
2013-06-26 wenzelm 2013-06-26 less intrusive SELECT_GOAL: merely rearrange subgoals without detaching goal state, and thus preserve maxidx context; even less intrusive PREFER_GOAL (without structural goal marker), e.g. relevant for generic_simp_tac; adapted ZF proof that broke for unknown reasons (potentially slight change of Drule.size_of_thm);
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-04-10 wenzelm 2013-04-10 obsolete -- tools should refer to proper Proof.context;
2013-03-30 wenzelm 2013-03-30 more formal cong_name;
2013-03-30 wenzelm 2013-03-30 more item markup; tuned signature;
2013-03-29 wenzelm 2013-03-29 Pretty.item markup for improved readability of lists of items;
2012-11-17 wenzelm 2012-11-17 tuned signature;
2012-08-11 wenzelm 2012-08-11 faster compilation of ML with antiquotations: static ML_context is bound once in auxiliary structure Isabelle;
2012-04-14 wenzelm 2012-04-14 outermost SELECT_GOAL potentially improves performance;
2012-03-31 wenzelm 2012-03-31 tuned signature;
2012-03-18 wenzelm 2012-03-18 maintain generic context naming in structure Name_Space (NB: empty = default_naming, init = local_naming); more explicit Context.generic for Name_Space.declare/define and derivatives (NB: naming changed after Proof_Context.init_global); prefer Context.pretty in low-level operations of structure Sorts/Type (defer full Syntax.init_pretty until error output); simplified signatures;
2012-03-17 wenzelm 2012-03-17 proper naming of simprocs according to actual target context; afford pervasive declaration which makes results available with qualified name from outside;
2012-03-03 wenzelm 2012-03-03 tuned;
2012-02-14 wenzelm 2012-02-14 tuned signature;
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 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-11-06 wenzelm 2011-11-06 more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute; misc tuning;
2011-11-03 wenzelm 2011-11-03 tuned -- Variable.declare_term is already part of Variable.auto_fixes;
2011-10-28 wenzelm 2011-10-28 uniform Local_Theory.declaration with explicit params;
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-27 wenzelm 2011-06-27 ML antiquotations are managed as theory data, with proper name space and entity markup; clarified Name_Space.check;
2011-05-13 wenzelm 2011-05-13 clarified map_simpset versus Simplifier.map_simpset_global;
2011-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-04-23 wenzelm 2011-04-23 added Name_Space.check/get convenience;
2011-04-23 wenzelm 2011-04-23 clarified check_simproc (with report) vs. the_simproc; proper report for @{simproc} (NB: ML environment is built in invisible context); only one data slot for this module;
2011-04-23 wenzelm 2011-04-23 proper binding/report of defined simprocs; tuned signature;
2011-04-17 wenzelm 2011-04-17 report Name_Space.declare/define, relatively to context; added "global" variants of context-dependent declarations;
2011-04-16 wenzelm 2011-04-16 PARALLEL_GOALS for method "simp_all";
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-12-22 haftmann 2010-12-22 tuned comment