src/HOL/Tools/Qelim/cooper.ML
2014-08-16 wenzelm 2014-08-16 updated to named_theorems;
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-03-21 wenzelm 2014-03-21 more qualified names;
2013-12-31 wenzelm 2013-12-31 proper context for norm_hhf and derived operations; clarified tool context in some boundary cases;
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-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-05-24 wenzelm 2013-05-24 tuned signature;
2013-05-17 wenzelm 2013-05-17 proper option quick_and_dirty;
2013-05-11 wenzelm 2013-05-11 prefer explicitly qualified exceptions, which is particular important for robust handlers;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2013-02-15 haftmann 2013-02-15 two target language numeral types: integer and natural, as replacement for code_numeral; former theory HOL/Library/Code_Numeral_Types replaces HOL/Code_Numeral; refined stack of theories implementing int and/or nat by target language numerals; reduced number of target language numeral types to exactly one
2012-12-03 hoelzl 2012-12-03 add check to Cooper's algorithm that left-hand of dvd is a numeral
2012-04-14 wenzelm 2012-04-14 refined Cooper.tac / "presburger" method: Subgoal.FOCUS_PARAMS allows to solve more problems with outer quantifiers, e.g "!!x. [| 0 <= (x::int); x div 2 < f x |] ==> x < f x * 2"; clarified thin_prems_tac: fail as tactic without error;
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)
2012-02-15 wenzelm 2012-02-15 renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
2011-12-02 wenzelm 2011-12-02 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-10-19 wenzelm 2011-10-19 inlined @{thms} (ML compile-time) allows to get rid of legacy zadd_ac as well (cf. 49e305100097);
2011-08-10 wenzelm 2011-08-10 old term operations are legacy;
2011-06-29 wenzelm 2011-06-29 modernized some simproc setup;
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-05-13 wenzelm 2011-05-13 proper Proof.context for classical tactics; reduced claset to snapshot of classical context; discontinued clasimpset;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-04-08 wenzelm 2011-04-08 explicit structure Syntax_Trans; discontinued old-style constrainAbsC;
2011-01-08 wenzelm 2011-01-08 misc tuning and comments based on review of Theory_Data, Proof_Data, Generic_Data usage;
2010-09-06 wenzelm 2010-09-06 more antiquotations;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 wenzelm 2010-08-27 more antiquotations;
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 haftmann 2010-08-26 formerly unnamed infix impliciation now named HOL.implies
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-06-08 haftmann 2010-06-08 tuned quotes, antiquotations and whitespace
2010-05-25 wenzelm 2010-05-25 eliminated various catch-all exception patterns, guessing at the concrete exeptions that are intended here;
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-11 haftmann 2010-05-11 represent de-Bruin indices simply by position in list
2010-05-11 haftmann 2010-05-11 tuned reification functions
2010-05-11 haftmann 2010-05-11 tuned code; toward a tightended interface with generated code
2010-05-10 haftmann 2010-05-10 tuned; dropped strange myassoc2
2010-05-10 haftmann 2010-05-10 stylized COOPER exception
2010-05-10 haftmann 2010-05-10 simplified oracle
2010-05-10 haftmann 2010-05-10 shorten names
2010-05-10 haftmann 2010-05-10 only one module fpr presburger method
2010-05-10 haftmann 2010-05-10 one structure is better than three
2010-05-10 haftmann 2010-05-10 less complex organization of cooper source code
2010-05-10 haftmann 2010-05-10 dropped unused bindings; avoid open (documents dependency on generated code more explicitly)
2010-05-06 haftmann 2010-05-06 merged
2010-05-06 haftmann 2010-05-06 tuned whitespace; dropped superfluous open
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-04-28 haftmann 2010-04-28 modernized structure name
2010-02-28 wenzelm 2010-02-28 more antiquotations;
2010-02-19 haftmann 2010-02-19 moved remaning class operations from Algebras.thy to Groups.thy
2010-02-10 haftmann 2010-02-10 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-10-21 haftmann 2009-10-21 curried union as canonical list operation
2009-10-21 haftmann 2009-10-21 merged
2009-10-21 haftmann 2009-10-21 dropped redundant gen_ prefix