Mercurial
isabelle
/ file revisions
summary
|
shortlog
|
changelog
|
graph
|
tags
|
branches
|
file
| revisions |
annotate
|
diff
|
rss
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