src/Pure/meta_simplifier.ML
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.
2001-05-09 nipkow 2001-05-09 improved simproc trace IGNORED
2001-01-03 wenzelm 2001-01-03 Thm: dest_comb, dest_abs, capply, cabs no longer global;
2000-11-07 berghofe 2000-11-07 Added new file meta_simplifier.ML