src/Pure/meta_simplifier.ML
2005-09-02 haftmann 2005-09-02 some 'assoc' etc. refactoring
2005-08-31 wenzelm 2005-08-31 refer to theory instead of low-level tsig;
2005-08-16 nipkow 2005-08-16 simp_depth warning now mod 20, not mod 10 (too often)
2005-08-01 wenzelm 2005-08-01 improved bounds: nameless Term.bound, recover names for output;
2005-07-28 wenzelm 2005-07-28 Term.bound;
2005-07-15 wenzelm 2005-07-15 tuned fold on terms;
2005-07-14 wenzelm 2005-07-14 tuned;
2005-07-13 wenzelm 2005-07-13 export eq_rrule; improved Net interface;
2005-07-01 wenzelm 2005-07-01 decomp_simp: compare terms, not cterms;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory;
2005-06-13 nipkow 2005-06-13 changed -1 back to 0
2005-06-12 nipkow 2005-06-12 simp_depth now starts at -1 to make it start at 0 ;-)
2005-06-06 nipkow 2005-06-06 Added the t = x "fix" - in (* ... *) :-(
2005-05-23 nipkow 2005-05-23 tuned trace info (depth)
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-24 berghofe 2005-01-24 Removed unnecessary subsignature checks to speed up rewriting.
2004-10-18 berghofe 2004-10-18 Replaced list of bound variables in simpset by maximal index of bound variables. This allows new variable names to be generated more quickly (without calling variant).
2004-09-11 nipkow 2004-09-11 undoing previous change
2004-09-10 nipkow 2004-09-10 new forward deduction capability for simplifier
2004-07-30 wenzelm 2004-07-30 tuned output;
2004-07-11 wenzelm 2004-07-11 improved print_ss; tuned;
2004-07-08 wenzelm 2004-07-08 major cleanup; got rid of obsolete meta_simpset;
2004-06-30 skalberg 2004-06-30 Made simplification procedures simpset-aware.
2004-06-25 skalberg 2004-06-25 Merging the meta-simplifier with the Provers-simplifier. Next step: make the simplification procedure simpset-aware.
2004-06-23 skalberg 2004-06-23 Moved conversion rules from MetaSimplifier to Drule. refl_implies removed from Drule, instead imp_cong' exported from there.
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-04-22 wenzelm 2004-04-22 tuned;
2003-12-25 nipkow 2003-12-25 Added trace msg
2003-10-21 skalberg 2003-10-21 Added access to the mk_rews field (and friends).
2003-05-20 kleing 2003-05-20 be less verbose about simplification depth
2003-04-28 ballarin 2003-04-28 Simplifier no longer aborts on failed congruence proof.
2003-02-27 ballarin 2003-02-27 Change to meta simplifier: congruence rules may now have frees as head of term.
2003-02-25 nipkow 2003-02-25 added simp_depth_limit
2002-10-21 berghofe 2002-10-21 No more explicit manipulation of flex-flex constraints in goals_conv.
2002-10-01 berghofe 2002-10-01 Deleted superfluous dest_implies.
2002-09-30 berghofe 2002-09-30 Completely reimplemented mutual simplification of premises.
2002-09-19 nipkow 2002-09-19 drule: added nRS simplifier: trace with names
2002-08-08 wenzelm 2002-08-08 exception SIMPROC_FAIL: solid error reporting of simprocs;
2002-08-05 wenzelm 2002-08-05 protect simplifier operation against spurious exceptions from simprocs;
2002-05-31 berghofe 2002-05-31 Changed interface of rewrite_term.
2002-02-28 wenzelm 2002-02-28 decomp_simp': use lhs instead of elhs (preserves more bound variable names);
2002-01-16 wenzelm 2002-01-16 interface to Pattern.rewrite_term;
2002-01-16 wenzelm 2002-01-16 export beta_eta_conversion;
2001-12-27 wenzelm 2001-12-27 tuned tracing markup;
2001-11-24 wenzelm 2001-11-24 gen_merge_lists;
2001-11-21 wenzelm 2001-11-21 use tracing function for trace output;
2001-11-12 berghofe 2001-11-12 congc now returns None if congruence rule has no effect.
2001-10-22 wenzelm 2001-10-22 Display.pretty_thms;
2001-10-14 wenzelm 2001-10-14 tuned rewrite/simplify interface;
2001-10-14 wenzelm 2001-10-14 tuned;
2001-10-12 berghofe 2001-10-12 Tuned comment.
2001-10-12 berghofe 2001-10-12 - Exported goals_conv and fconv_rule - Added forall_conv
2001-10-04 wenzelm 2001-10-04 removed obsolete comment;
2001-10-04 wenzelm 2001-10-04 full_rewrite_cterm_aux (see also tactic.ML); no longer open MetaSimplifier;
2001-08-28 nipkow 2001-08-28 Implemented indentation schema for conditional rewrite trace.
2001-08-23 nipkow 2001-08-23 Traced depth of conditional rewriting
2001-06-11 berghofe 2001-06-11 Fixed bug in function rebuild.
2001-05-10 nipkow 2001-05-10 improved tracing of permutative rules.