src/HOL/Tools/arith_data.ML
2012-03-25 huffman 2012-03-25 merged fork with new numeral representation (see NEWS)
2011-11-23 wenzelm 2011-11-23 modernized some old-style infix operations, which were left over from the time of ML proof scripts;
2011-10-28 wenzelm 2011-10-28 tuned Named_Thms: proper binding;
2011-09-17 haftmann 2011-09-17 tuned
2011-04-16 wenzelm 2011-04-16 modernized structure Proof_Context;
2011-01-13 wenzelm 2011-01-13 less verbosity -- avoid slightly odd tracing information on warning channel;
2010-08-25 wenzelm 2010-08-25 renamed Simplifier.simproc(_i) to Simplifier.simproc_global(_i) to emphasize that this is not the real thing;
2010-03-13 wenzelm 2010-03-13 reverted fe9b43a08187 -- "warning" is a perfectly normal way of tactics to emit spurious messages (although "arith" could be less chatty), while "priority" is a special Proof General protocol message;
2010-03-07 huffman 2010-03-07 arith tactic uses 'priority' instead of 'warning' to print messages
2010-02-28 wenzelm 2010-02-28 more antiquotations;
2010-02-19 haftmann 2010-02-19 moved remaning class operations from Algebras.thy to Groups.thy
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2010-01-28 haftmann 2010-01-28 new theory Algebras.thy for generic algebraic structures
2009-11-10 wenzelm 2009-11-10 eliminated some unused/obsolete Args.bang_facts;
2009-11-08 wenzelm 2009-11-08 adapted Theory_Data; tuned;
2009-10-30 haftmann 2009-10-30 dedicated theory for loading numeral simprocs
2009-10-17 wenzelm 2009-10-17 explicitly qualify Drule.standard;
2009-07-23 wenzelm 2009-07-23 more @{theory} antiquotations;
2009-07-02 wenzelm 2009-07-02 renamed NamedThmsFun to Named_Thms; simplified/unified names of instances of Named_Thms;
2009-04-06 haftmann 2009-04-06 tuned comment
2009-03-26 wenzelm 2009-03-26 simplified attribute and method setup: eliminating bottom-up styles makes it easier to keep things in one place, and also SML/NJ happy;
2009-03-23 haftmann 2009-03-23 moved generic arith_tac (formerly silent_arith_tac), verbose_arith_tac (formerly arith_tac) to Arith_Data; simple_arith-tac now named linear_arith_tac
2009-03-13 haftmann 2009-03-13 moved some generic nonsense to arith_data.ML
2009-03-12 haftmann 2009-03-12 vague cleanup in arith proof tools setup: deleted dead code, more proper structures, clearer arrangement
2009-01-01 wenzelm 2009-01-01 normalized some ML type/val aliases;
2008-12-03 haftmann 2008-12-03 made repository layout more coherent with logical distribution structure; stripped some $Id$s