src/ZF/int_arith.ML
2016-04-08 wenzelm 2016-04-08 eliminated unused simproc identifier;
2015-10-10 wenzelm 2015-10-10 tuned syntax -- more symbols;
2015-09-09 wenzelm 2015-09-09 simplified simproc programming interfaces;
2015-03-19 wenzelm 2015-03-19 slightly more formal historic examples;
2015-02-11 wenzelm 2015-02-11 proper context; tuned whitespace;
2014-08-21 haftmann 2014-08-21 integrated appendix theory into main theory; tuned ML
2013-11-11 wenzelm 2013-11-11 tuned signature -- removed obsolete Addsimprocs, Delsimprocs;
2013-04-18 wenzelm 2013-04-18 simplifier uses proper Proof.context instead of historic type simpset;
2011-09-17 haftmann 2011-09-17 dropped unused argument – avoids problem with SML/NJ
2010-12-02 wenzelm 2010-12-02 renamed trace_simp to simp_trace, and debug_simp to simp_debug;
2010-11-03 wenzelm 2010-11-03 eliminated dead code;
2010-11-03 wenzelm 2010-11-03 more conventional exceptions for abstract syntax operations -- eliminated ancient SYS_ERROR; proper signature constraint;
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-02-28 wenzelm 2010-02-28 more antiquotations; eliminated legacy ML bindings;
2010-02-27 wenzelm 2010-02-27 modernized structure Term_Ord;
2010-02-13 wenzelm 2010-02-13 modernized structures;
2010-02-11 wenzelm 2010-02-11 numeral syntax: clarify parse trees vs. actual terms; modernized translations; formal markup of @{syntax_const} and @{const_syntax};
2010-02-07 wenzelm 2010-02-07 prefer explicit @{lemma} over adhoc forward reasoning;
2009-10-17 wenzelm 2009-10-17 explicitly qualify Drule.standard;
2009-07-23 wenzelm 2009-07-23 more @{theory} antiquotations;
2009-07-23 wenzelm 2009-07-23 renamed simpset_of to global_simpset_of, and local_simpset_of to simpset_of -- same for claset and clasimpset;
2009-03-20 wenzelm 2009-03-20 eliminated global SIMPSET, CLASET etc. -- refer to explicit context;
2008-12-31 wenzelm 2008-12-31 moved term order operations to structure TermOrd (cf. Pure/term_ord.ML); tuned signature of structure Term;
2008-06-16 wenzelm 2008-06-16 converted ML proofs;
2008-06-11 wenzelm 2008-06-11 OldGoals.inst;
2008-03-01 wenzelm 2008-03-01 tuned ML code, more antiquotations;
2008-02-11 wenzelm 2008-02-11 removed unnecessary theory qualifiers;
2008-02-11 krauss 2008-02-11 Made theory names in ZF disjoint from HOL theory names to allow loading both developments in a single session (but not merge them).
2007-10-07 wenzelm 2007-10-07 modernized specifications; removed legacy ML bindings;
2007-09-18 wenzelm 2007-09-18 simplified type int (eliminated IntInf.int, integer);
2007-05-31 wenzelm 2007-05-31 moved Integ files to canonical place;