src/HOL/Tools/Qelim/cooper.ML
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
2009-10-20 haftmann 2009-10-20 replaced old_style infixes eq_set, subset, union, inter and variants by generic versions
2009-10-21 wenzelm 2009-10-21 standardized basic operations on type option;
2009-10-19 wenzelm 2009-10-19 uniform use of Integer.add/mult/sum/prod;
2009-09-18 haftmann 2009-09-18 tuned const_name antiquotations
2009-08-28 wenzelm 2009-08-28 modernized messages -- eliminated old Display.print_cterm;
2009-08-24 boehmes 2009-08-24 stricter condition for (binary) integer relation
2009-07-28 haftmann 2009-07-28 Set.UNIV and Set.empty are mere abbreviations for top and bot
2009-05-11 haftmann 2009-05-11 qualified names for Lin_Arith tactics and simprocs
2009-03-23 haftmann 2009-03-23 moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
2009-03-19 wenzelm 2009-03-19 proper spacing before ML antiquotations -- note that @ may be part of symbolic ML identifiers;
2009-03-11 haftmann 2009-03-11 tuned funny error message
2009-03-05 haftmann 2009-03-05 set operations Int, Un, INTER, UNION, Inter, Union, empty, UNIV are now proper qualified constants with authentic syntax
2009-02-03 haftmann 2009-02-03 regenerated presburger code
2008-12-31 wenzelm 2008-12-31 moved old add_term_vars, add_term_frees etc. to structure OldTerm;
2008-09-29 wenzelm 2008-09-29 handle _ should be avoided (spurious Interrupt will spoil the game);
2008-09-18 wenzelm 2008-09-18 simplified oracle interface;
2008-07-18 haftmann 2008-07-18 moved op dvd to theory Ring_and_Field; generalized a couple of lemmas
2008-06-23 wenzelm 2008-06-23 Logic.all/mk_equals/mk_implies;
2008-05-29 wenzelm 2008-05-29 proper context for simp_thms_conv;
2008-05-17 wenzelm 2008-05-17 structure Display: less pervasive operations;
2008-01-02 haftmann 2008-01-02 some more antiquotations
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated IntInf.int, integer);
2007-09-15 haftmann 2007-09-15 fixed title
2007-08-16 wenzelm 2007-08-16 removed dead code;
2007-07-31 wenzelm 2007-07-31 arith method setup: proper context;
2007-07-20 haftmann 2007-07-20 moved class ord from Orderings.thy to HOL.thy
2007-07-10 haftmann 2007-07-10 now works with SML/NJ