src/HOL/arith_data.ML
2008-02-20 haftmann 2008-02-20 tuned structures in arith_data.ML
2007-11-28 haftmann 2007-11-28 dropped dead code
2007-07-31 wenzelm 2007-07-31 moved lin_arith stuff to Tools/lin_arith.ML;
2007-07-31 wenzelm 2007-07-31 arith method setup: proper context; turned fast_arith_split/neq_limit into configuration options; tuned signatures; misc cleanup;
2007-07-20 haftmann 2007-07-20 moved class ord from Orderings.thy to HOL.thy
2007-07-03 wenzelm 2007-07-03 CONVERSION tactical;
2007-06-13 huffman 2007-06-13 removed constant int :: nat => int; int is now an abbreviation for of_nat :: nat => int
2007-06-02 webertj 2007-06-02 cosmetic
2007-06-01 webertj 2007-06-01 fixed handling of meta-logic propositions
2007-05-24 nipkow 2007-05-24 Introduced new classes monoid_add and group_add
2007-05-17 haftmann 2007-05-17 canonical prefixing of class constants
2007-05-13 haftmann 2007-05-13 refined module rat
2007-05-10 haftmann 2007-05-10 fixed typo
2007-05-10 wenzelm 2007-05-10 moved conversions to structure Conv;
2007-05-09 haftmann 2007-05-09 tuned
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-05-06 haftmann 2007-05-06 tuned
2007-04-11 haftmann 2007-04-11 canonical merge operations
2007-03-29 haftmann 2007-03-29 dropped legacy ML bindings
2006-12-18 haftmann 2006-12-18 switched argument order in *.syntax lifters
2006-12-13 haftmann 2006-12-13 introduced mk/dest_numeral/number for mk/dest_binum etc.
2006-12-01 haftmann 2006-12-01 slight cleanup in hologic.ML
2006-11-18 haftmann 2006-11-18 op div/op mod now named without leading op
2006-11-08 wenzelm 2006-11-08 removed theory NatArith (now part of Nat);
2006-10-09 wenzelm 2006-10-09 attribute: Context.mapping;
2006-10-04 nipkow 2006-10-04 fixed bug in linear arith
2006-10-04 webertj 2006-10-04 nnf_simpset built statically
2006-09-26 haftmann 2006-09-26 renamed 0 and 1 to HOL.zero and HOL.one respectivly; introduced corresponding syntactic classes
2006-09-06 haftmann 2006-09-06 got rid of Numeral.bin type
2006-08-25 webertj 2006-08-25 avoid duplicate tactics
2006-08-24 webertj 2006-08-24 additional list of tactics that can be added to arith
2006-08-02 webertj 2006-08-02 type annotations fixed (IntInf.int, to make SML/NJ happy)
2006-08-01 webertj 2006-08-01 possible disagreement between proof search and proof reconstruction when eliminating inequalities over different types fixed
2006-07-31 webertj 2006-07-31 fixed a bug in function poly: decomposition of products
2006-07-31 webertj 2006-07-31 code reformatted
2006-07-29 webertj 2006-07-29 lin_arith_prover splits certain operators (e.g. min, max, abs)
2006-07-26 webertj 2006-07-26 linear arithmetic splits certain operators (e.g. min, max, abs)
2006-07-08 wenzelm 2006-07-08 simprocs: no theory argument -- use simpset context instead;
2006-06-08 nipkow 2006-06-08 replaced REPEAT by REPOEAT_DETERM
2006-04-27 paulson 2006-04-27 renamed HOLogic.mk_bin to mk_binum for consistency with dest_binum
2006-03-21 paulson 2006-03-21 Removal of unnecessary simprules: simproc cancel_numerals now works without add_Suc, while the reason for the horrible isolateSuc is not known.
2006-03-17 nipkow 2006-03-17 fixed problem with proof reconstruction by adding add_Suc to arith-simpset.
2006-03-17 haftmann 2006-03-17 renamed op < <= to Orderings.less(_eq)
2006-03-10 haftmann 2006-03-10 renamed HOL + - * etc. to HOL.plus HOL.minus HOL.times etc.
2006-02-15 webertj 2006-02-15 typo in a comment fixed
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2005-12-13 chaieb 2005-12-13 simpset for computation in raw_arith_tac added just as comment, nothing changed!
2005-12-01 wenzelm 2005-12-01 simprocs: static evaluation of simpset;
2005-10-25 wenzelm 2005-10-25 EVERY;
2005-10-25 wenzelm 2005-10-25 avoid legacy goals;
2005-10-21 wenzelm 2005-10-21 OldGoals;
2005-10-21 haftmann 2005-10-21 introduced functions from Pure/General/rat.ML
2005-10-17 wenzelm 2005-10-17 change_claset/simpset; Simplifier.inherit_context instead of Simplifier.inherit_bounds;
2005-09-23 wenzelm 2005-09-23 Provers/Arith/fast_lin_arith.ML: Simplifier.inherit_bounds;
2005-09-12 haftmann 2005-09-12 introduced new-style AList operations
2005-08-01 wenzelm 2005-08-01 tuned msg;
2005-07-14 wenzelm 2005-07-14 HOL.Not; tuned;
2005-07-07 nipkow 2005-07-07 linear arithmetic now takes "&" in assumptions apart.
2005-06-20 wenzelm 2005-06-20 get_thm instead of obsolete Goals.get_thm; improved msg;