isabelle: File revisions

src/HOL/Tools/numeral_simprocs.ML

2014-05-30	nipkow	2014-05-30	must not cancel common factors on both sides of (in)equations in linear arithmetic decicision procedure	file \| diff \| annotate
2014-03-25	wenzelm	2014-03-25	eliminated dead code;	file \| diff \| annotate
2013-11-19	haftmann	2013-11-19	eliminiated neg_numeral in favour of - (numeral _)	file \| diff \| annotate
2013-11-01	haftmann	2013-11-01	more simplification rules on unary and binary minus	file \| diff \| annotate
2013-04-18	wenzelm	2013-04-18	simplifier uses proper Proof.context instead of historic type simpset;	file \| diff \| annotate
2012-09-12	wenzelm	2012-09-12	standardized ML aliases;	file \| diff \| annotate
2012-03-25	huffman	2012-03-25	merged fork with new numeral representation (see NEWS)	file \| diff \| annotate
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;	file \| diff \| annotate
2012-01-17	huffman	2012-01-17	factor-cancellation simprocs now call the full simplifier to prove that factors are non-zero	file \| diff \| annotate
2011-11-28	huffman	2011-11-28	use HOL_basic_ss instead of HOL_ss for internal simproc proofs (cf. b36eedcd1633)	file \| diff \| annotate
2011-11-24	wenzelm	2011-11-24	modernized some old-style infix operations, which were left over from the time of ML proof scripts;	file \| diff \| annotate
2011-11-23	wenzelm	2011-11-23	modernized some old-style infix operations, which were left over from the time of ML proof scripts;	file \| diff \| annotate
2011-11-09	huffman	2011-11-09	tune post-processing of simproc-generated rules so they won't produce Numeral0 or Numeral1	file \| diff \| annotate
2011-10-29	huffman	2011-10-29	remove unused function	file \| diff \| annotate
2011-10-28	huffman	2011-10-28	use simproc_setup for cancellation simprocs, to get proper name bindings	file \| diff \| annotate
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**	file \| diff \| annotate
2011-09-18	huffman	2011-09-18	merged	file \| diff \| annotate
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	file \| diff \| annotate
2011-09-17	haftmann	2011-09-17	dropped unused argument – avoids problem with SML/NJ	file \| diff \| annotate
2011-09-17	haftmann	2011-09-17	tuned	file \| diff \| annotate
2011-08-08	huffman	2011-08-08	moved division ring stuff from Rings.thy to Fields.thy	file \| diff \| annotate
2010-12-02	wenzelm	2010-12-02	renamed trace_simp to simp_trace, and debug_simp to simp_debug;	file \| diff \| annotate
2010-08-28	haftmann	2010-08-28	formerly unnamed infix equality now named HOL.eq	file \| diff \| annotate
2010-08-19	haftmann	2010-08-19	use antiquotations for remaining unqualified constants in HOL	file \| diff \| annotate
2010-07-19	haftmann	2010-07-19	diff_minus subsumes diff_def	file \| diff \| annotate
2010-05-15	wenzelm	2010-05-15	less pervasive names from structure Thm;	file \| diff \| annotate
2010-05-07	haftmann	2010-05-07	split of semiring normalization from Groebner theory; moved field_comp_conv to Numeral_Simproces	file \| diff \| annotate
2010-04-26	haftmann	2010-04-26	use new classes (linordered_)field_inverse_zero	file \| diff \| annotate
2010-04-26	haftmann	2010-04-26	class division_ring_inverse_zero	file \| diff \| annotate
2010-03-27	boehmes	2010-03-27	slightly more general simproc (avoids errors of linarith)	file \| diff \| annotate
2010-02-27	wenzelm	2010-02-27	modernized structure Term_Ord;	file \| diff \| annotate
2010-02-19	haftmann	2010-02-19	moved remaning class operations from Algebras.thy to Groups.thy	file \| diff \| annotate
2010-02-10	haftmann	2010-02-10	moved less_eq, less to Orderings.thy; moved abs, sgn to Groups.thy	file \| diff \| annotate
2010-02-10	haftmann	2010-02-10	moved constants inverse and divide to Ring.thy	file \| diff \| annotate
2010-02-09	haftmann	2010-02-09	hide fact names clashing with fact names from Group.thy	file \| diff \| annotate
2010-02-08	haftmann	2010-02-08	renamed OrderedGroup to Groups; split theory Ring_and_Field into Rings Fields	file \| diff \| annotate
2010-02-08	haftmann	2010-02-08	dropped accidental duplication of "lin" prefix from cs. 108662d50512	file \| diff \| annotate
2010-02-08	haftmann	2010-02-08	merged	file \| diff \| annotate
2010-02-05	haftmann	2010-02-05	more consistent naming of type classes involving orderings (and lattices) -- c.f. NEWS	file \| diff \| annotate
2010-02-07	wenzelm	2010-02-07	prefer explicit @{lemma} over adhoc forward reasoning;	file \| diff \| annotate
2010-01-28	haftmann	2010-01-28	new theory Algebras.thy for generic algebraic structures	file \| diff \| annotate
2009-10-30	haftmann	2009-10-30	dedicated theory for loading numeral simprocs	file \| diff \| annotate
2009-10-17	wenzelm	2009-10-17	explicitly qualify Drule.standard;	file \| diff \| annotate
2009-07-23	wenzelm	2009-07-23	more @{theory} antiquotations;	file \| diff \| annotate
2009-06-02	wenzelm	2009-06-02	made SML/NJ happy;	file \| diff \| annotate
2009-05-11	haftmann	2009-05-11	qualified names for Lin_Arith tactics and simprocs	file \| diff \| annotate
2009-05-08	haftmann	2009-05-08	modules numeral_simprocs, nat_numeral_simprocs; proper structures for numeral simprocs	file \| diff \| annotate \| base

isabelle

RSS Atom