src/Pure/meta_simplifier.ML
2009-11-24 haftmann 2009-11-24 curried take/drop
2009-11-08 wenzelm 2009-11-08 tuned;
2009-11-02 wenzelm 2009-11-02 back to warning -- Proof General tends to "popup" tracing output;
2009-10-29 wenzelm 2009-10-29 less aggressive tracing;
2009-10-27 wenzelm 2009-10-27 eliminated some old folds;
2009-10-21 haftmann 2009-10-21 merged
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-20 wenzelm 2009-10-20 backpatching of structure Proof and ProofContext -- avoid odd aliases; renamed transfer_proof to raw_transfer; indicate firm naming conventions for theory, Proof.context, Context.generic;
2009-10-20 wenzelm 2009-10-20 uniform use of Integer.min/max;
2009-09-30 wenzelm 2009-09-30 eliminated dead code; eliminated redundant bindings; misc tuning;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-05-30 wenzelm 2009-05-30 tuned;
2009-04-21 krauss 2009-04-21 replace type cong = {thm : thm, lhs : term} by plain thm -- the other component has been unused for a long time.
2009-03-16 wenzelm 2009-03-16 provide Simplifier.norm_hhf(_protect) as regular simplifier operation;
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-03-06 wenzelm 2009-03-06 replaced archaic use of rep_ss by Simplifier.mksimps;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-11-18 wenzelm 2008-11-18 eliminated rewrite_tac/fold_tac, which are not well-formed tactics due to change of main conclusion; eliminated obsolete alias rewtac for rewrite_goals_tac;
2008-10-16 wenzelm 2008-10-16 Drule.norm_hhf_eqs;
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-07-14 haftmann 2008-07-14 dropped junk
2008-07-14 haftmann 2008-07-14 added further simple interfaces
2008-06-21 wenzelm 2008-06-21 activate_context: strict the_context, no fallback on theory context;
2008-05-29 wenzelm 2008-05-29 legacy_feature: no proof context in simpset;
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2008-03-27 wenzelm 2008-03-27 eliminated theory ProtoPure;
2007-11-27 berghofe 2007-11-27 check_conv now only performs beta-eta-normalization when equations cannot be combined just by transitivity.
2007-10-26 wenzelm 2007-10-26 asm_rewrite_goal_tac: avoiding PRIMITIVE lets informative exceptions (from simprocs) get through;
2007-09-25 wenzelm 2007-09-25 Syntax.parse/check/read;
2007-08-20 wenzelm 2007-08-20 tuned merge operations via pointer_eq;
2007-08-02 wenzelm 2007-08-02 turned simp_depth_limit into configuration option;
2007-07-23 wenzelm 2007-07-23 depth flag: plain bool ref; eliminated transform_failure (to avoid critical section for main transactions);
2007-07-05 wenzelm 2007-07-05 tuned;
2007-07-05 wenzelm 2007-07-05 tuned goal conversion interfaces;
2007-07-03 wenzelm 2007-07-03 moved (asm_)rewrite_goal_tac from goal.ML to meta_simplifier.ML (no longer depends on SELECT_GOAL);
2007-06-03 wenzelm 2007-06-03 merge_ss: plain merge of prems;
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2007-05-10 wenzelm 2007-05-10 moved some Drule operations to Thm (see more_thm.ML);
2007-05-09 wenzelm 2007-05-09 simp_depth: now proper value in simpset (prevents problems with lost exception trace, enables multi-threaded simplification); trace_simp_depth_limit_exceeded: attempt to hide destructive pointer programming within simpset;
2007-04-16 haftmann 2007-04-16 canonical merge operations
2007-04-14 wenzelm 2007-04-14 Morphism.transform/form;
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-02-06 wenzelm 2007-02-06 trace/debug: avoid eager string concatenation;
2007-02-04 wenzelm 2007-02-04 type simproc: explicitl dependency of morphism; added eq_simproc, morph_simproc; renamed mk_simproc' to make_simproc -- primary interface;
2007-01-31 haftmann 2007-01-31 changed cong alist - now using AList operations instead of overwrite_warn
2007-01-04 wenzelm 2007-01-04 added mk_simproc': tuned interface; tuned runtime context: merge with dynamic one;
2006-12-30 wenzelm 2006-12-30 removed conditional combinator;
2006-12-07 wenzelm 2006-12-07 reorganized structure Tactic vs. MetaSimplifier;
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
2006-11-30 wenzelm 2006-11-30 qualified MetaSimplifier.norm_hhf(_protect);
2006-11-29 wenzelm 2006-11-29 simplified Logic.count_prems;
2006-11-28 wenzelm 2006-11-28 simplified '?' operator;
2006-11-24 wenzelm 2006-11-24 ProofContext.init;
2006-11-10 haftmann 2006-11-10 introduces canonical AList functions for loop_tacs
2006-10-11 haftmann 2006-10-11 abandoned findrep
2006-10-09 wenzelm 2006-10-09 Drule.lhs/rhs_of;
2006-09-21 wenzelm 2006-09-21 member (op =); Drule.dest_equals_rhs;