src/HOL/Decision_Procs/ferrack_tac.ML
2014-03-21 wenzelm 2014-03-21 more qualified names;
2014-02-14 wenzelm 2014-02-14 proper signature; removed dead code;
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-05-24 wenzelm 2013-05-24 tuned signature;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-04-12 wenzelm 2012-04-12 more standard method setup;
2012-03-27 huffman 2012-03-27 remove redundant lemmas
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-11-27 wenzelm 2011-11-27 more antiquotations;
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-03-24 wenzelm 2011-03-24 added Term.is_open and Term.is_dependent convenience, to cover common situations of loose bounds;
2010-08-19 haftmann 2010-08-19 tuned quotes
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-12 haftmann 2010-05-12 modernized specifications; tuned reification
2010-05-05 haftmann 2010-05-05 farewell to old-style mem infixes -- type inference in situations with mem_int and mem_string should provide enough information to resolve the type of (op =)
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-02-19 wenzelm 2010-02-19 local Simplifier.context; tuned tactic setup;
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-19 wenzelm 2009-10-19 always qualify NJ's old List.foldl/foldr in Isabelle/ML;
2009-10-17 wenzelm 2009-10-17 eliminated hard tabulators, guessing at each author's individual tab-width; tuned headers;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-06-24 nipkow 2009-06-24 corrected and unified thm names
2009-05-30 wenzelm 2009-05-30 proper signature constraint; modernized method setup;
2009-03-13 wenzelm 2009-03-13 unified type Proof.method and pervasive METHOD combinators;
2009-03-11 hoelzl 2009-03-11 Updated paths in Decision_Procs comments and NEWS
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-04 blanchet 2009-03-04 Merge.
2009-03-03 nipkow 2009-03-03 removed and renamed redundant lemmas
2009-02-21 nipkow 2009-02-21 removed redundant thms
2009-02-17 nipkow 2009-02-17 Cleaned up IntDiv and removed subsumed lemmas.
2009-02-06 haftmann 2009-02-06 session Reflecion renamed to Decision_Procs, moved Dense_Linear_Order there