src/Provers/Arith/fast_lin_arith.ML
2016-06-04 wenzelm 2016-06-04 Integer.lcm normalizes the sign as in HOL/GCD.thy; tuned;
2016-06-01 wenzelm 2016-06-01 tuned signature;
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 dropped dead code
2015-04-10 wenzelm 2015-04-10 tuned signature;
2015-03-09 wenzelm 2015-03-09 eliminated dead code (cf. 5e5c36b051af);
2015-03-06 wenzelm 2015-03-06 clarified context;
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 clarified signature;
2015-03-04 wenzelm 2015-03-04 tuned;
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;
2014-11-26 wenzelm 2014-11-26 renamed "pairself" to "apply2", in accordance to @{apply 2};
2014-10-30 wenzelm 2014-10-30 eliminated aliases;
2014-02-09 nipkow 2014-02-09 disabled counterexample output for now; confusing because often incorrect
2013-05-24 wenzelm 2013-05-24 tuned signature;
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;
2012-09-15 haftmann 2012-09-15 dropped some unused identifiers
2012-03-21 wenzelm 2012-03-21 prefer explicitly qualified exception List.Empty;
2012-02-27 wenzelm 2012-02-27 clarified prems_lin_arith_tac, with subtle change of semantics: structured prems are inserted as well;
2011-09-02 wenzelm 2011-09-02 proper config option linarith_trace;
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 tuned signature;
2011-06-27 blanchet 2011-06-27 clarify warning message to avoid confusing beginners
2011-06-09 wenzelm 2011-06-09 tuned signature: Name.invent and Name.invent_names;
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-01-10 wenzelm 2011-01-10 added merge_options convenience;
2010-11-03 wenzelm 2010-11-03 replaced ancient sys_error by raise Fail, assuming that the latter is not handled specifically by the environment;
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-07-28 haftmann 2010-07-28 dropped dead code
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-22 boehmes 2010-03-22 removed warning_count (known causes for warnings have been resolved)
2010-03-22 boehmes 2010-03-22 removed e-mail address from error message
2010-03-13 wenzelm 2010-03-13 removed old CVS Ids; tuned headers;
2010-03-09 hoelzl 2010-03-09 Use same order of neq-elimination as in proof search.
2010-02-19 wenzelm 2010-02-19 Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-10-29 wenzelm 2009-10-29 standardized filter/filter_out;
2009-10-27 wenzelm 2009-10-27 eliminated some old folds;
2009-10-21 haftmann 2009-10-21 curried union as canonical list operation
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-19 wenzelm 2009-10-19 uniform use of Integer.add/mult/sum/prod;
2009-10-15 wenzelm 2009-10-15 replaced String.concat by implode; replaced String.concatWith by space_implode; replaced (Seq.flat o Seq.map) by Seq.maps; replaced List.mapPartial by map_filter; replaced List.concat by flat; replaced (flat o map) by maps, which produces less garbage;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-30 wenzelm 2009-07-30 qualified Subgoal.FOCUS;
2009-07-26 wenzelm 2009-07-26 replaced old METAHYPS by FOCUS;
2009-07-21 wenzelm 2009-07-21 proper context for Display.pretty_thm etc. or old-style versions Display.pretty_thm_global, Display.pretty_thm_without_context etc.;
2009-07-10 haftmann 2009-07-10 dropped find_index_eq
2009-06-15 haftmann 2009-06-15 made SML/NJ happy
2009-06-09 boehmes 2009-06-09 tuned
2009-06-08 boehmes 2009-06-08 fast_lin_arith uses proper multiplication instead of unfolding to additions