src/HOL/Decision_Procs/cooper_tac.ML
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-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-06-29 wenzelm 2011-06-29 modernized some simproc setup;
2011-04-16 wenzelm 2011-04-16 proper subgoal addressing via SUBGOAL/CSUBGOAL -- assuming these tactics did not handle Subscript in any special way; tuned;
2011-04-16 wenzelm 2011-04-16 eliminated old List.nth; tuned;
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-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;
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-25 wenzelm 2009-05-25 proper signature constraints; modernized method setup;
2009-05-08 haftmann 2009-05-08 dropped legacy ml theorem binding
2009-04-17 haftmann 2009-04-17 added both cancel_div_mod_procs
2009-03-13 wenzelm 2009-03-13 more regular method setup via SIMPLE_METHOD;
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-20 nipkow 2009-02-20 Removed redundant lemmas
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