src/Pure/meta_simplifier.ML
2010-05-15 ago less pervasive names from structure Thm;
2010-05-03 ago renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-30 ago conditional warnings: explicitly observe context visibility flag, not just accidental presence of a context;
2010-04-29 ago proper context for mksimps etc. -- via simpset of the running Simplifier;
2010-04-26 ago eliminanated some unreferenced identifiers;
2010-03-29 ago the configuration option 'trace_simp' now uses the reference of the ProofGeneral settings menu as (dynamic) default value
2010-03-28 ago static defaults for configuration options;
2010-03-27 ago re-introduce reference to control simplifier tracing (needed for ProofGeneral settings menu) (cf. 12bb31230550)
2010-03-26 ago replaced references 'trace_simp' and 'debug_simp' by configuration options stored in the context
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-02-27 ago modernized structure Term_Ord;
2010-02-19 ago renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2010-02-19 ago tuned message;
2009-11-25 ago normalized uncurry take/drop
2009-11-24 ago curried take/drop
2009-11-08 ago tuned;
2009-11-02 ago back to warning -- Proof General tends to "popup" tracing output;
2009-10-29 ago less aggressive tracing;
2009-10-27 ago eliminated some old folds;
2009-10-21 ago merged
2009-10-21 ago dropped redundant gen_ prefix
2009-10-20 ago replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-20 ago backpatching of structure Proof and ProofContext -- avoid odd aliases;
2009-10-20 ago uniform use of Integer.min/max;
2009-09-30 ago eliminated dead code;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-05-30 ago tuned;
2009-04-21 ago replace type cong = {thm : thm, lhs : term} by plain thm -- the other component has been unused for a long time.
2009-03-16 ago provide Simplifier.norm_hhf(_protect) as regular simplifier operation;
2009-03-08 ago added dest_ss;
2009-03-07 ago renamed rep_ss to MetaSimplifier.internal_ss;
2009-03-06 ago replaced archaic use of rep_ss by Simplifier.mksimps;
2008-12-31 ago moved term order operations to structure TermOrd (cf. Pure/term_ord.ML);
2008-11-18 ago eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion;
2008-10-16 ago Drule.norm_hhf_eqs;
2008-08-14 ago moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-07-14 ago dropped junk
2008-07-14 ago added further simple interfaces
2008-06-21 ago activate_context: strict the_context, no fallback on theory context;
2008-05-29 ago legacy_feature: no proof context in simpset;
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-04-12 ago rep_cterm/rep_thm: no longer dereference theory_ref;
2008-03-27 ago eliminated theory ProtoPure;
2007-11-27 ago check_conv now only performs beta-eta-normalization when equations
2007-10-26 ago asm_rewrite_goal_tac: avoiding PRIMITIVE lets informative exceptions (from simprocs) get through;
2007-09-25 ago Syntax.parse/check/read;
2007-08-20 ago tuned merge operations via pointer_eq;
2007-08-02 ago turned simp_depth_limit into configuration option;
2007-07-23 ago depth flag: plain bool ref;
2007-07-05 ago tuned;
2007-07-05 ago tuned goal conversion interfaces;
2007-07-03 ago moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
2007-06-03 ago merge_ss: plain merge of prems;
2007-05-31 ago simplified/unified list fold;
2007-05-10 ago moved some Drule operations to Thm (see more_thm.ML);
2007-05-09 ago simp_depth: now proper value in simpset (prevents problems with lost exception trace, enables multi-threaded simplification);
2007-04-16 ago canonical merge operations
2007-04-14 ago Morphism.transform/form;
2007-02-26 ago moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-02-06 ago trace/debug: avoid eager string concatenation;