src/HOL/Tools/numeral_simprocs.ML
2015-11-17 paulson 2015-11-17 Removed some legacy theorems; minor adjustments to simplification rules; new material on homotopic paths
2015-09-10 wenzelm 2015-09-10 tuned -- avoid slightly odd @{cpat};
2015-09-09 wenzelm 2015-09-09 simplified simproc programming interfaces;
2015-07-27 wenzelm 2015-07-27 tuned signature;
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-03-31 haftmann 2015-03-31 given up separate type classes demanding `inverse 0 = 0`
2015-03-20 paulson 2015-03-20 fixed crash in cancel_numeral_simprocs. NB they still don't work except for type nat!
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 signature -- prefer qualified names;
2015-02-19 haftmann 2015-02-19 establish unique preferred fact names
2015-02-18 haftmann 2015-02-18 eliminated technical fact alias
2015-02-11 wenzelm 2015-02-11 proper context; tuned whitespace;
2014-10-02 haftmann 2014-10-02 moved lemmas out of Int.thy which have nothing to do with int
2014-07-05 haftmann 2014-07-05 prefer ac_simps collections over separate name bindings for add and mult
2014-07-04 haftmann 2014-07-04 reduced name variants for assoc and commute on plus and mult
2014-05-30 nipkow 2014-05-30 must not cancel common factors on both sides of (in)equations in linear arithmetic decicision procedure
2014-03-25 wenzelm 2014-03-25 eliminated dead code;
2013-11-19 haftmann 2013-11-19 eliminiated neg_numeral in favour of - (numeral _)
2013-11-01 haftmann 2013-11-01 more simplification rules on unary and binary minus
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2012-09-12 wenzelm 2012-09-12 standardized ML aliases;
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;
2012-01-17 huffman 2012-01-17 factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero
2011-11-28 huffman 2011-11-28 use HOL_basic_ss instead of HOL_ss for internal simproc proofs (cf. b36eedcd1633)
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-11-09 huffman 2011-11-09 tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
2011-10-29 huffman 2011-10-29 remove unused function
2011-10-28 huffman 2011-10-28 use simproc_setup for cancellation simprocs, to get proper name bindings
2011-10-27 huffman 2011-10-27 fix bug in cancel_factor simprocs so they will work on goals like 'x * y < x * z' where the common term is already on the left
2011-09-18 huffman 2011-09-18 merged
2011-09-15 huffman 2011-09-15 numeral_simprocs.ML: use HOL_basic_ss instead of HOL_ss for internal normalization proofs of cancel_factor simprocs, to avoid splitting if-then-else
2011-09-17 haftmann 2011-09-17 dropped unused argument – avoids problem with SML/NJ
2011-09-17 haftmann 2011-09-17 tuned
2011-08-08 huffman 2011-08-08 moved division ring stuff from Rings.thy to Fields.thy
2010-12-02 wenzelm 2010-12-02 renamed trace_simp to simp_trace, and debug_simp to simp_debug;
2010-08-28 haftmann 2010-08-28 formerly unnamed infix equality now named HOL.eq
2010-08-19 haftmann 2010-08-19 use antiquotations for remaining unqualified constants in HOL
2010-07-19 haftmann 2010-07-19 diff_minus subsumes diff_def
2010-05-15 wenzelm 2010-05-15 less pervasive names from structure Thm;
2010-05-07 haftmann 2010-05-07 split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
2010-04-26 haftmann 2010-04-26 use new classes (linordered_)field_inverse_zero
2010-04-26 haftmann 2010-04-26 class division_ring_inverse_zero
2010-03-27 boehmes 2010-03-27 slightly more general simproc (avoids errors of linarith)
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
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-10 haftmann 2010-02-10 moved constants inverse and divide to Ring.thy
2010-02-09 haftmann 2010-02-09 hide fact names clashing with fact names from Group.thy
2010-02-08 haftmann 2010-02-08 renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
2010-02-08 haftmann 2010-02-08 dropped accidental duplication of "lin" prefix from cs. 108662d50512
2010-02-08 haftmann 2010-02-08 merged
2010-02-05 haftmann 2010-02-05 more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
2010-02-07 wenzelm 2010-02-07 prefer explicit @{lemma} over adhoc forward reasoning;
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-10-30 haftmann 2009-10-30 dedicated theory for loading numeral simprocs