src/HOL/Tools/lin_arith.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-07-27 huffman 2012-07-27 replace Nat_Arith simprocs with simpler conversions that do less rearrangement of terms
2012-07-27 huffman 2012-07-27 give Nat_Arith simprocs proper name bindings by using simproc_setup
2012-07-27 huffman 2012-07-27 replace abel_cancel simprocs with functionally equivalent, but simpler and faster ones
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2012-02-27 wenzelm 2012-02-27 clarified prems_lin_arith_tac, with subtle change of semantics: structured prems are inserted as well;
2011-12-02 wenzelm 2011-12-02 more antiquotations;
2011-11-24 wenzelm 2011-11-24 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
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-09-17 haftmann 2011-09-17 tuned spacing
2011-09-02 wenzelm 2011-09-02 proper config option linarith_trace;
2011-08-08 huffman 2011-08-08 moved division ring stuff from Rings.thy to Fields.thy
2011-06-30 wenzelm 2011-06-30 merged
2011-06-29 boehmes 2011-06-29 linarith counterexamples now provide only valuations for variables (which should restrict the number of linarith trace messages); control tracing of (potentially spurious) counterexamples by the configuration option "linarith_verbose" (to disable linarith traces entirely)
2011-06-29 wenzelm 2011-06-29 simplified/unified Simplifier.mk_solver;
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-02 wenzelm 2011-05-02 added Attrib.setup_config_XXX conveniences, with implicit setup of the background theory; proper name bindings;
2011-04-20 wenzelm 2011-04-20 eliminated Display.string_of_thm_without_context; tuned whitespace;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-01-08 wenzelm 2011-01-08 tuned;
2010-12-17 wenzelm 2010-12-17 refer to regular structure Simplifier;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-27 wenzelm 2010-08-27 merged, resolving some minor conflicts in src/HOL/Tools/Predicate_Compile/code_prolog.ML;
2010-08-27 haftmann 2010-08-27 formerly unnamed infix conjunction and disjunction now named HOL.conj and HOL.disj
2010-08-26 wenzelm 2010-08-26 Fast_Lin_Arith.number_of: more conventional merge that prefers the left side -- note that former ordering wrt. serial numbers makes it depend on accidental load order;
2010-08-26 wenzelm 2010-08-26 slightly more abstract data handling in Fast_Lin_Arith;
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
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-07-19 haftmann 2010-07-19 modernized abel_cancel simproc setup
2010-07-19 haftmann 2010-07-19 discontinued pretending that abel_cancel is logic-independent; cleaned up junk
2010-06-08 haftmann 2010-06-08 tuned quotes, antiquotations and whitespace
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-28 wenzelm 2010-03-28 static defaults for configuration options;
2010-03-22 boehmes 2010-03-22 removed warning_count (known causes for warnings have been resolved)
2010-03-07 wenzelm 2010-03-07 modernized structure Object_Logic;
2010-02-28 wenzelm 2010-02-28 more antiquotations;
2010-02-22 haftmann 2010-02-22 merged
2010-02-19 haftmann 2010-02-19 moved remaning class operations from Algebras.thy to Groups.thy
2010-02-19 wenzelm 2010-02-19 renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;
2010-02-19 wenzelm 2010-02-19 Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;
2010-02-10 haftmann 2010-02-10 moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
2010-02-10 haftmann 2010-02-10 moved constants inverse and divide to Ring.thy
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-11-17 webertj 2009-11-17 Fixed splitting of div and mod on integers (split theorem differed from implementation).
2009-11-16 webertj 2009-11-16 Fixed a typo in a comment.
2009-11-10 wenzelm 2009-11-10 eliminated some unused/obsolete Args.bang_facts;
2009-11-08 wenzelm 2009-11-08 tuned;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
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-10-02 wenzelm 2009-10-02 eliminated dead code; tuned;
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-14 webertj 2009-08-14 Fixed a bug where the simplifier would hang on lemma "f a = M { nat j |j. 0 <= j & j < f b}" pre_decomp/pre_tac no longer split terms that contain (non-locally) bound variables (e.g., "nat j" in the above example).