src/HOL/Tools/lin_arith.ML
23 months ago nipkow 2017-09-07 more simp power and less incompleteness or arith
2017-06-08 boehmes 2017-06-08 replace non-arithmetic terms by fresh variables before replaying linear-arithmetic proofs: avoid failed proof replays due to an overambitious simpset which may cause proof replay to diverge from the pre-computed proof trace
2016-09-26 haftmann 2016-09-26 syntactic type class for operation mod named after mod; simplified assumptions of type class semiring_div
2016-09-26 haftmann 2016-09-26 dropped tautological pattern
2016-09-26 haftmann 2016-09-26 more warning comments
2016-06-01 wenzelm 2016-06-01 more adhoc overloading; eliminated pointless Rat.eq: this is an equality type; tuned;
2016-06-01 wenzelm 2016-06-01 clarified exception -- actually reject denominator = 0;
2016-06-01 wenzelm 2016-06-01 prefer rat numberals;
2016-06-01 wenzelm 2016-06-01 tuned signature;
2016-02-17 haftmann 2016-02-17 consolidated name
2015-12-13 wenzelm 2015-12-13 more general types Proof.method / context_tactic; proper context for Method.insert_tac; tuned;
2015-09-25 wenzelm 2015-09-25 moved remaining display.ML to more_thm.ML;
2015-09-09 wenzelm 2015-09-09 simplified simproc programming interfaces;
2015-09-02 wenzelm 2015-09-02 trim context for persistent storage;
2015-07-05 wenzelm 2015-07-05 simplified Thm.instantiate and derivatives: the LHS refers to non-certified variables -- this merely serves as index into already certified structures (or is ignored);
2015-06-01 haftmann 2015-06-01 separate class for division operator, with particular syntax added in more specific classes
2015-06-01 haftmann 2015-06-01 explicit check for field sort, to anticipate situation where syntactic checking alone will not be sufficient any longer
2015-06-01 haftmann 2015-06-01 dropped dead config option
2015-06-01 haftmann 2015-06-01 tuned, including proper signature for functor argument
2015-04-10 wenzelm 2015-04-10 tuned signature;
2015-03-09 wenzelm 2015-03-09 eliminated unused arith "verbose" flag -- tools that need options can use the context;
2015-03-09 wenzelm 2015-03-09 eliminated dead code (cf. 5e5c36b051af);
2015-03-06 wenzelm 2015-03-06 Thm.cterm_of and Thm.ctyp_of operate on local context;
2015-03-04 wenzelm 2015-03-04 tuned signature -- prefer qualified names;
2015-02-10 wenzelm 2015-02-10 proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.; occasionally clarified use of context;
2015-01-11 wenzelm 2015-01-11 tuned warnings: observe Context_Position.is_visible;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-11-09 wenzelm 2014-11-09 proper context for compose_tac, Splitter.split_tac (relevant for unify trace options);
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-09-21 wenzelm 2014-09-21 more standard Isabelle/ML operations;
2014-08-16 wenzelm 2014-08-16 clarified order of arith rules;
2014-08-16 wenzelm 2014-08-16 updated to named_theorems;
2014-03-07 wenzelm 2014-03-07 more antiquotations;
2014-02-10 nipkow 2014-02-10 improved lin.arith. for terms involving division
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-11-04 haftmann 2013-11-04 streamlined setup of linear arithmetic
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;