isabelle: File revisions

src/HOL/Numeral_Simprocs.thy

2015-03-31	haftmann	2015-03-31	given up separate type classes demanding `inverse 0 = 0`	file \| diff \| annotate
2015-03-20	paulson	2015-03-20	fixed crash in cancel_numeral_simprocs. NB they still don't work except for type nat!	file \| diff \| annotate
2014-11-02	wenzelm	2014-11-02	modernized header uniformly as section;	file \| diff \| annotate
2014-02-10	nipkow	2014-02-10	improved lin.arith. for terms involving division	file \| diff \| annotate
2013-11-19	haftmann	2013-11-19	eliminiated neg_numeral in favour of - (numeral _)	file \| diff \| annotate
2013-11-04	haftmann	2013-11-04	streamlined setup of linear arithmetic	file \| diff \| annotate
2012-08-22	wenzelm	2012-08-22	prefer ML_file over old uses;	file \| diff \| annotate
2012-04-01	huffman	2012-04-01	removed Nat_Numeral.thy, moving all theorems elsewhere	file \| diff \| annotate
2012-03-27	huffman	2012-03-27	generalize some theorems about div/mod	file \| diff \| annotate
2012-03-25	huffman	2012-03-25	merged fork with new numeral representation (see NEWS)	file \| diff \| annotate
2011-11-20	wenzelm	2011-11-20	eliminated obsolete "standard";	file \| diff \| annotate
2011-11-11	huffman	2011-11-11	use simproc_setup for the remaining nat_numeral simprocs	file \| diff \| annotate
2011-11-11	huffman	2011-11-11	use simproc_setup for more nat_numeral simprocs; add simproc tests	file \| diff \| annotate
2011-11-09	huffman	2011-11-09	use simproc_setup for some nat_numeral simprocs; add simproc tests	file \| diff \| annotate
2011-11-09	huffman	2011-11-09	add ring_char_0 class constraints to several simprocs (internal proofs of #n ~= 0 fail for type s not in this class); test simprocs using most general type classes instead of just int and rat.	file \| diff \| annotate
2011-10-30	huffman	2011-10-30	*extend cancellation simproc patterns to cover terms like '- (2 pi) < pi'**	file \| diff \| annotate
2011-10-28	huffman	2011-10-28	more accurate class constraints on cancellation simproc patterns	file \| diff \| annotate
2011-10-28	huffman	2011-10-28	use simproc_setup for cancellation simprocs, to get proper name bindings	file \| diff \| annotate
2010-07-19	haftmann	2010-07-19	tuned whitespace	file \| diff \| annotate
2009-10-30	haftmann	2009-10-30	dedicated theory for loading numeral simprocs	file \| diff \| annotate

isabelle

RSS Atom