src/HOL/Tools/numeral_simprocs.ML
Tue, 31 Mar 2015 21:54:32 +0200 haftmann given up separate type classes demanding `inverse 0 = 0`
Fri, 20 Mar 2015 14:00:22 +0000 paulson fixed crash in cancel_numeral_simprocs. NB they still don't work except for type nat!
Fri, 06 Mar 2015 23:56:43 +0100 wenzelm clarified context;
Fri, 06 Mar 2015 15:58:56 +0100 wenzelm Thm.cterm_of and Thm.ctyp_of operate on local context;
Wed, 04 Mar 2015 22:05:01 +0100 wenzelm clarified signature;
Wed, 04 Mar 2015 19:53:18 +0100 wenzelm tuned signature -- prefer qualified names;
Thu, 19 Feb 2015 11:53:36 +0100 haftmann establish unique preferred fact names
Wed, 18 Feb 2015 22:46:48 +0100 haftmann eliminated technical fact alias
Wed, 11 Feb 2015 11:18:36 +0100 wenzelm proper context;
Thu, 02 Oct 2014 11:33:06 +0200 haftmann moved lemmas out of Int.thy which have nothing to do with int
Sat, 05 Jul 2014 11:01:53 +0200 haftmann prefer ac_simps collections over separate name bindings for add and mult
Fri, 04 Jul 2014 20:18:47 +0200 haftmann reduced name variants for assoc and commute on plus and mult
Fri, 30 May 2014 18:13:40 +0200 nipkow must not cancel common factors on both sides of (in)equations in linear arithmetic decicision procedure
Tue, 25 Mar 2014 19:13:33 +0100 wenzelm eliminated dead code;
Tue, 19 Nov 2013 10:05:53 +0100 haftmann eliminiated neg_numeral in favour of - (numeral _)
Fri, 01 Nov 2013 18:51:14 +0100 haftmann more simplification rules on unary and binary minus
Thu, 18 Apr 2013 17:07:01 +0200 wenzelm simplifier uses proper Proof.context instead of historic type simpset;
Wed, 12 Sep 2012 13:56:49 +0200 wenzelm standardized ML aliases;
Sun, 25 Mar 2012 20:15:39 +0200 huffman merged fork with new numeral representation (see NEWS)
Wed, 15 Feb 2012 23:19:30 +0100 wenzelm renamed Thm.capply to Thm.apply, and Thm.cabs to Thm.lambda in conformance with similar operations in structure Term and Logic;
Tue, 17 Jan 2012 16:30:54 +0100 huffman factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero
Mon, 28 Nov 2011 21:28:01 +0100 huffman use HOL_basic_ss instead of HOL_ss for internal simproc proofs (cf. b36eedcd1633)
Thu, 24 Nov 2011 21:01:06 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Wed, 23 Nov 2011 22:59:39 +0100 wenzelm modernized some old-style infix operations, which were left over from the time of ML proof scripts;
Wed, 09 Nov 2011 15:33:24 +0100 huffman tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1
Sat, 29 Oct 2011 10:00:35 +0200 huffman remove unused function
Fri, 28 Oct 2011 11:02:27 +0200 huffman use simproc_setup for cancellation simprocs, to get proper name bindings
Thu, 27 Oct 2011 07:46:57 +0200 huffman 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
Sun, 18 Sep 2011 16:12:43 -0700 huffman merged
Thu, 15 Sep 2011 10:12:36 -0700 huffman 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
Sat, 17 Sep 2011 15:08:55 +0200 haftmann dropped unused argument – avoids problem with SML/NJ
Sat, 17 Sep 2011 00:37:21 +0200 haftmann tuned
Mon, 08 Aug 2011 09:52:09 -0700 huffman moved division ring stuff from Rings.thy to Fields.thy
Thu, 02 Dec 2010 16:04:22 +0100 wenzelm renamed trace_simp to simp_trace, and debug_simp to simp_debug;
Sat, 28 Aug 2010 16:14:32 +0200 haftmann formerly unnamed infix equality now named HOL.eq
Thu, 19 Aug 2010 11:02:14 +0200 haftmann use antiquotations for remaining unqualified constants in HOL
Mon, 19 Jul 2010 16:09:44 +0200 haftmann diff_minus subsumes diff_def
Sat, 15 May 2010 21:50:05 +0200 wenzelm less pervasive names from structure Thm;
Fri, 07 May 2010 15:05:52 +0200 haftmann split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces
Mon, 26 Apr 2010 15:37:50 +0200 haftmann use new classes (linordered_)field_inverse_zero
Mon, 26 Apr 2010 11:34:17 +0200 haftmann class division_ring_inverse_zero
Sat, 27 Mar 2010 02:10:00 +0100 boehmes slightly more general simproc (avoids errors of linarith)
Sat, 27 Feb 2010 23:13:01 +0100 wenzelm modernized structure Term_Ord;
Fri, 19 Feb 2010 14:47:01 +0100 haftmann moved remaning class operations from Algebras.thy to Groups.thy
Wed, 10 Feb 2010 14:12:04 +0100 haftmann moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy
Wed, 10 Feb 2010 08:49:26 +0100 haftmann moved constants inverse and divide to Ring.thy
Tue, 09 Feb 2010 11:47:47 +0100 haftmann hide fact names clashing with fact names from Group.thy
Mon, 08 Feb 2010 17:12:38 +0100 haftmann renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields
Mon, 08 Feb 2010 14:22:22 +0100 haftmann dropped accidental duplication of "lin" prefix from cs. 108662d50512
Mon, 08 Feb 2010 11:13:30 +0100 haftmann merged
Fri, 05 Feb 2010 14:33:50 +0100 haftmann more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS
Sun, 07 Feb 2010 19:31:55 +0100 wenzelm prefer explicit @{lemma} over adhoc forward reasoning;
Thu, 28 Jan 2010 11:48:49 +0100 haftmann new theory Algebras.thy for generic algebraic structures
Fri, 30 Oct 2009 13:59:51 +0100 haftmann dedicated theory for loading numeral simprocs
Sat, 17 Oct 2009 00:52:37 +0200 wenzelm explicitly qualify Drule.standard;
Thu, 23 Jul 2009 23:12:21 +0200 wenzelm more @{theory} antiquotations;
Tue, 02 Jun 2009 16:52:37 +0200 wenzelm made SML/NJ happy;
Mon, 11 May 2009 15:57:29 +0200 haftmann qualified names for Lin_Arith tactics and simprocs
Fri, 08 May 2009 09:48:07 +0200 haftmann modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs
less more (0) tip