src/Pure/simplifier.ML
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
2010-12-17 wenzelm 2010-12-17 more explicit references to structure Raw_Simplifier;
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-12-17 wenzelm 2010-12-17 clarified exports of structure Simplifier;
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-06-15 haftmann 2010-06-15 tuned whitespace
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-30 wenzelm 2010-04-30 export Simplifier.with_context;
2010-04-30 wenzelm 2010-04-30 conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context; map_ss: explicitly provide a temporary context, which might be required for mksimps, mkcongs etc.;
2010-04-29 wenzelm 2010-04-29 proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-03-06 wenzelm 2010-03-06 eliminated Args.bang_facts (legacy feature);
2010-02-19 wenzelm 2010-02-19 renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
2009-11-10 wenzelm 2009-11-10 define simprocs: do not apply target_morphism prematurely, this is already done in LocalTheory.declaration;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-05 wenzelm 2009-11-05 adapted LocalTheory.declaration;
2009-10-25 wenzelm 2009-10-25 LocalTheory.naming_of;
2009-10-25 wenzelm 2009-10-25 make SML/NJ happy;
2009-10-24 wenzelm 2009-10-24 maintain explicit name space kind; export Name_Space.the_entry; tuned messages;
2009-10-24 wenzelm 2009-10-24 renamed NameSpace to Name_Space -- also to emphasize its subtle change in semantics;
2009-10-24 wenzelm 2009-10-24 eliminated separate stamp -- NameSpace.define/merge etc. ensure uniqueness already;
2009-09-30 wenzelm 2009-09-30 eliminated dead code;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-05-30 wenzelm 2009-05-30 modernized method setup; tuned;
2009-03-20 wenzelm 2009-03-20 Disposed old declarations, tactics, tactic combinators that refer to the simpset or claset of an implicit theory;
2009-03-15 wenzelm 2009-03-15 simplified attribute setup;
2009-03-13 wenzelm 2009-03-13 eliminated type Args.T; pervasive types 'a parser and 'a context_parser;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-12 wenzelm 2009-03-12 renamed NameSpace.bind to NameSpace.define;
2009-03-08 wenzelm 2009-03-08 added dest_ss; proper context fo pretty_ss; tuned;
2009-03-07 wenzelm 2009-03-07 renamed rep_ss to MetaSimplifier.internal_ss;
2009-01-21 wenzelm 2009-01-21 removed Ids;