src/HOL/Tools/TFL/rules.ML
2013-12-14 wenzelm 2013-12-14 proper context for basic Simplifier operations: rewrite_rule, rewrite_goals_rule, rewrite_goals_tac etc.; clarified tool context in some boundary cases;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
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-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-08-08 wenzelm 2011-08-08 misc tuning -- eliminated old-fashioned rep_thm;
2011-08-02 krauss 2011-08-02 moved recursion combinator to HOL/Library/Wfrec.thy -- it is so fundamental and well-known that it should survive recdef
2011-08-02 krauss 2011-08-02 moved recdef package to HOL/Library/Old_Recdef.thy
2011-06-29 wenzelm 2011-06-29 tuned signature;
2011-06-09 wenzelm 2011-06-09 renamed Drule.instantiate to Drule.instantiate_normalize to emphasize its meaning as opposed to plain Thm.instantiate;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2010-12-17 wenzelm 2010-12-17 renamed structure MetaSimplifier to raw_Simplifer, to emphasize its meaning;
2010-12-17 wenzelm 2010-12-17 refer to regular structure Simplifier;
2010-12-15 wenzelm 2010-12-15 avoid ML structure aliases (especially single-letter abbreviations);
2010-08-27 wenzelm 2010-08-27 disposed some old debugging tools;
2010-08-19 haftmann 2010-08-19 corrected some long-overseen misperceptions in recdef
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-07-01 haftmann 2010-07-01 "prod" and "sum" replace "*" and "+" respectively
2010-06-10 haftmann 2010-06-10 tuned quotes, antiquotations and whitespace
2010-05-26 haftmann 2010-05-26 dropped legacy theorem bindings
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-03 wenzelm 2010-05-03 UNDISCH/DISJ_CASESL: eliminated slightly odd Thm.legacy_freezeT -- these rules appear to be applied to thms with fixed types only;
2010-05-03 wenzelm 2010-05-03 renamed Thm.freezeT to Thm.legacy_freezeT -- it is based on Type.legacy_freeze;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
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-10-29 wenzelm 2009-10-29 eliminated some old folds;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-18 haftmann 2009-09-18 tuned const_name antiquotations
2009-08-31 krauss 2009-08-31 moved wfrec to Recdef.thy
2009-08-28 wenzelm 2009-08-28 modernized messages -- eliminated old Display.print_cterm;
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-07-06 wenzelm 2009-07-06 structure Thm: less pervasive names;
2009-03-01 wenzelm 2009-03-01 use long names for old-style fold combinators;
2009-01-01 wenzelm 2009-01-01 normalized some ML type/val aliases;
2008-12-31 wenzelm 2008-12-31 moved old add_type_XXX, add_term_XXX etc. to structure OldTerm;
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-04-26 krauss 2008-04-26 fixed recdef, broken by my previous commit
2008-04-12 wenzelm 2008-04-12 rep_cterm/rep_thm: no longer dereference theory_ref;
2007-05-31 wenzelm 2007-05-31 moved TFL files to canonical place;